Commit 2026-07-10 02:42 1a783458

View on Github →

feat(Algebra/Algebra/Tower): add restrictScalarsHom (#41417) This PR adds AlgEquiv.restrictScalarsHom, analogous to the existing AlgEquiv.extendScalarsHomOfSurjective. This PR also renames coe_restrictScalars -> toRingEquiv_restrictScalars without a deprecation to make way for coe_restrictScalars' -> coe_restrictScalars.

Estimated changes

Modified Mathlib/Algebra/Algebra/Tower.lean

deleted theorem AlgEquiv.coe_restrictScalars'

modified theorem AlgEquiv.coe_restrictScalars

added def AlgEquiv.restrictScalarsHom

added theorem AlgEquiv.restrictScalarsHom_apply

added theorem AlgEquiv.restrictScalarsHom_injective

added theorem AlgEquiv.symm_restrictScalars

added theorem AlgEquiv.toMonoidHom_symm_extendScalarsHomOfSurjective

added theorem AlgEquiv.toRingEquiv_restrictScalars

Modified Mathlib/RingTheory/Smooth/IntegralClosure.lean