Theorem minpoly.IsIntegrallyClosed.degree_le_of_ne_zero
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) …
Modified minpoly.IsIntegrallyClosed.degree_le_of_ne_zeroView on Github →