Commit 2025-07-21 19:28 8a8c0c1a

View on Github →

feat: API for Minpoly.toAdjoin and friends (#27278)

Replace simps! invocations on AdjoinRoot.Minpoly.toAdjoin and minpoly.equivAdjoin with principled API
Create API for AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly The auto-generated simps! lemmas unfolded the expressions too far for simp to be able to continue simplifying them. A good example of the difference is the proof of Minpoly.toAdjoin.apply_X.

Estimated changes

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

added theorem minpoly.coe_equivAdjoin

added theorem minpoly.equivAdjoin_toAlgHom

Modified Mathlib/RingTheory/Adjoin/Field.lean

added theorem AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom

added theorem AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.Minpoly.coe_toAdjoin

added theorem AdjoinRoot.Minpoly.coe_toAdjoin_mk_X

deleted theorem AdjoinRoot.Minpoly.toAdjoin.apply_X

deleted theorem AdjoinRoot.Minpoly.toAdjoin_apply'