Theorem Irreducible.dvd_iff_aeval_eq_zero

Modification history

2026-07-28 14:29
Mathlib/FieldTheory/Minpoly/Field.lean
feat(FieldTheory/Finite): irreducible polynomial divides X^q^n - X iff degree divides n (#39239)
Added Irreducible.dvd_iff_aeval_eq_zeroView on Github →