Commit 2023-10-05 06:34 d926a388

View on Github →

chore(RingTheory): golf, generalize, fix docs (#7500)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Point.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

modified theorem minpoly.isIntegrallyClosed_dvd

modified theorem minpoly.isIntegrallyClosed_dvd_iff

Modified Mathlib/FieldTheory/Normal.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

modified theorem AdjoinRoot.mk_surjective