2025-11-09 22:22
Mathlib/FieldTheory/Minpoly/Field.lean
feat(FieldTheory/Minpoly/IsIntegrallyClosed): if an element is the root of a polynomial of minimal degree which is monic up to a constant then it is integral (#31412) …
Added minpoly.unique_of_degree_le_degree_minpoly