Commit 2026-03-23 12:40 a97f32d3

feat(FieldTheory/Finite): irreducible factors of X^q^n - X have degree dividing n (#36414) Add the theorem that if an irreducible polynomial over a finite field K divides X ^ (Fintype.card K) ^ n - X, then the degree of the polynomial divides n. We also add an auxiliary lemma stating that polynomials of nonzero degree dividing X ^ (Fintype.card K) - X have a root in K.