Commit 2026-04-19 10:51 b3edd5d4

View on Github →

chore(Algebra/Category): add ModuleCat.restrictScalarsIsoOfEquiv (#37773) Extracted from #37766 as a separate PR, because it also contains three basic simp lemmas. We also add missing type annotations in the file Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

modified def ModuleCat.ExtendRestrictScalarsAdj.Counit.map

modified def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars

modified def ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars

modified def ModuleCat.ExtendRestrictScalarsAdj.Unit.map

modified def ModuleCat.ExtendRestrictScalarsAdj.homEquiv

modified def ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction

modified def ModuleCat.restrictScalarsEquivalenceOfRingEquiv

added def ModuleCat.restrictScalarsIsoOfEquiv

added theorem ModuleCat.restrictScalarsIsoOfEquiv_hom_apply

added theorem ModuleCat.restrictScalarsIsoOfEquiv_inv_apply

Modified Mathlib/Algebra/Module/RingHom.lean

added theorem RingHom.toModule_smul

Modified Mathlib/Algebra/Polynomial/Module/Basic.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

added theorem RingEquiv.coe_coe_toAddEquiv_symm

added theorem RingEquiv.coe_coe_toEquiv_symm

added theorem RingEquiv.coe_coe_toMulEquiv_symm

Modified Mathlib/RingTheory/Perfection.lean