mathlib3

1acf2b9a - feat(is_cyclotomic_extension/basic): add is_cyclotomic_extension.equiv (#16757)

feat(is_cyclotomic_extension/basic): add is_cyclotomic_extension.equiv (#16757) We add `add is_cyclotomic_extension.equiv`: being a cyclotomic extension is preserved by `alg_equiv`, and others lemmas about cyclotomic extensions. From flt-regular