Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-27 07:38 1acf2b9a

View on Github →

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

Estimated changes

Modified src/number_theory/cyclotomic/basic.lean

added def is_cyclotomic_extension.alg_equiv

added theorem is_cyclotomic_extension.equiv

modified theorem is_cyclotomic_extension.finite

modified theorem is_cyclotomic_extension.finite_dimensional

modified theorem is_cyclotomic_extension.finite_of_singleton

added theorem is_cyclotomic_extension.iff_union_of_dvd

added theorem is_cyclotomic_extension.iff_union_singleton_one

modified theorem is_cyclotomic_extension.integral

modified theorem is_cyclotomic_extension.number_field

added theorem is_cyclotomic_extension.of_union_of_dvd

added theorem is_cyclotomic_extension.singleton_one_of_algebra_map_bijective

added theorem is_cyclotomic_extension.singleton_one_of_bot_eq_top

added theorem is_cyclotomic_extension.singleton_zero_of_bot_eq_top

modified theorem is_cyclotomic_extension.trans

Modified src/number_theory/cyclotomic/primitive_roots.lean

Modified src/number_theory/cyclotomic/rat.lean