Theorem minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd
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.isIntegral_iff_leadingCoeff_dvdView on Github →