Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 15:04 e8713864

View on Github →

feat(number_theory/cyclotomic/basic): add lemmas (#11264) From flt-regular.

Estimated changes

Modified src/number_theory/cyclotomic/basic.lean

added theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots

added theorem is_cyclotomic_extension.finite_dimensional

added theorem is_cyclotomic_extension.integral

added theorem is_cyclotomic_extension.splits_X_pow_sub_one

added theorem is_cyclotomic_extension.splits_cyclotomic

added theorem is_cyclotomic_extension.splitting_field_X_pow_sub_one

added theorem is_cyclotomic_extension.splitting_field_cyclotomic