Theorem minpoly.IsIntegrallyClosed.unique_of_degree_le_degree_minpoly
Modification history
2025-11-09 22:22
Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.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.IsIntegrallyClosed.unique_of_degree_le_degree_minpolyView on Github →