Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 3cd9088b

View on Github →

feat(ring_theory/polynomial/cyclotomic/basic): add lemmas (#11266) From flt-regular.

Estimated changes

Modified src/algebra/ne_zero.lean

added theorem ne_zero.not_dvd_char

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

added theorem polynomial.cyclotomic_mul_prime_dvd_eq_pow

added theorem polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd

added theorem polynomial.cyclotomic_mul_prime_pow_eq

added theorem polynomial.is_root_cyclotomic_iff_char_zero

added theorem polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p