mathlib

d58ce5ac - feat(number_theory/cyclotomic/zeta): add is_cyclotomic_extension.zeta (#11695)

feat(number_theory/cyclotomic/zeta): add is_cyclotomic_extension.zeta (#11695) We add `is_cyclotomic_extension.zeta n A B`: any primitive `n`-th root of unity in a cyclotomic extension. From flt-regular.