Commit 2023-06-16 17:43 006e3f6a

View on Github →

feat: port RingTheory.Polynomial.Cyclotomic.Expand (#5145)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean

added theorem Polynomial.cyclotomic_expand_eq_cyclotomic

added theorem Polynomial.cyclotomic_expand_eq_cyclotomic_mul

added theorem Polynomial.cyclotomic_irreducible_of_irreducible_pow

added theorem Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow

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.isRoot_cyclotomic_prime_pow_mul_iff_of_charP