Theorem Polynomial.Irreducible.natDegree_dvd_finrank

Modification history

2026-03-23 12:40
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
feat(FieldTheory/Finite): irreducible factors of X^q^n - X have degree dividing n (#36414) …
Added Polynomial.Irreducible.natDegree_dvd_finrankView on Github →