mathlib

ae5b6952 - refactor(number_theory/cyclotomic/*): refactor the definition of is_cyclotomic_extension (#14463)

refactor(number_theory/cyclotomic/*): refactor the definition of is_cyclotomic_extension (#14463) We modify the definition of `is_cyclotomic_extension`, requiring the existence of a primitive root of unity rather than a root of the cyclotomic polynomial. This removes almost all the `ne_zero` assumptions.