Theorem Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X

Modification history

2026-10-17 10:25
Mathlib/FieldTheory/Finite/Extension.lean
refactor: move results about polynomial degrees outside of the `FiniteField` namespace (#44691) …
Modified Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_XView on Github →
2026-07-28 14:29
Mathlib/FieldTheory/Finite/Extension.lean
feat(FieldTheory/Finite): irreducible polynomial divides X^q^n - X iff degree divides n (#39239)
Modified Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_XView on Github →
2026-03-23 12:40
Mathlib/FieldTheory/Finite/Extension.lean
feat(FieldTheory/Finite): irreducible factors of X^q^n - X have degree dividing n (#36414) …
Added Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_XView on Github →