Theorem Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_X

Modification history

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)
Added Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_XView on Github →