mathlib

5e48b217 - feat(number_theory/cyclotomic/basic): add cyclotomic_field and cyclotomic_ring (#11383)

feat(number_theory/cyclotomic/basic): add cyclotomic_field and cyclotomic_ring (#11383) We add `cyclotomic_field` and `cyclotomic_ring`, that provide an explicit cyclotomic extension of a given field/ring. From flt-regular