Theorem minpoly.Irreducible.eq_minpoly

Modification history

2026-03-23 12:40
Mathlib/FieldTheory/Minpoly/Field.lean
feat(FieldTheory/Finite): irreducible factors of X^q^n - X have degree dividing n (#36414) …
Added minpoly.Irreducible.eq_minpolyView on Github →