Commit 2026-07-28 14:29 9d302fc7

View on Github →

feat(FieldTheory/Finite): irreducible polynomial divides X^q^n - X iff degree divides n (#39239)

Estimated changes

Modified Mathlib/FieldTheory/Finite/Extension.lean

added theorem Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_X

modified theorem Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X

Modified Mathlib/FieldTheory/Minpoly/Field.lean

added theorem Irreducible.dvd_iff_aeval_eq_zero