Commit 2025-10-07 08:33 ef24a29f

View on Github →

feat: factorization of cyclotomic polynomial over finite fields (#30032) We compute the degree of the factors of the n-th cyclotomic polynomial over a finite field of characteristic p when p and n are coprime.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/CharAndCard.lean

modified theorem charP_of_card_eq_prime

added theorem charP_of_card_eq_prime_pow

modified theorem not_isUnit_prime_of_dvd_card

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

deleted theorem Polynomial.separable_cyclotomic

Modified Mathlib/NumberTheory/GaussSum.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

added theorem Polynomial.separable_cyclotomic

added theorem Polynomial.squarefree_cyclotomic

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

added theorem Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree

added theorem Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible

added theorem Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic

added theorem Polynomial.normalizedFactors_cyclotomic_card

added theorem ZMod.irreducible_of_dvd_cyclotomic_of_natDegree