Commit 2025-11-09 22:22 5d2ad00e
View on Github →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)
and versions of minpoly.unique given p.degree ≤ minpoly.degree.