mathlib3

2f3b966f - feat(number_theory/cyclotomic/basic): add is_cyclotomic_extension (#10849)

feat(number_theory/cyclotomic/basic): add is_cyclotomic_extension (#10849) We add a class `is_cyclotomic_extension S A B` expressing the fact that `B` is obtained by `A` by adding `n`-th primitive roots of unity, for all `n ∈ S`, where `S : set ℕ+`, and some basic properties. We will add more properties of cyclotomic extensions in a future work. From flt-regular.