Commit 2021-12-27 16:46 2f3b966f

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.