Commit 2024-03-24 09:49 08172593

View on Github →

chore(Algebra/Category/MonCat): improve definitional properties in restrict scalars (#11597) Replaces two usages of subst by an explicit construction in ChangeOfRings.

Estimated changes

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

added def ModuleCat.restrictScalarsComp'App

added theorem ModuleCat.restrictScalarsComp'App_hom_apply

added theorem ModuleCat.restrictScalarsComp'App_inv_apply

deleted theorem ModuleCat.restrictScalarsComp'_hom_apply

deleted theorem ModuleCat.restrictScalarsComp'_inv_apply

modified def ModuleCat.restrictScalarsId'

added def ModuleCat.restrictScalarsId'App

added theorem ModuleCat.restrictScalarsId'App_hom_apply

added theorem ModuleCat.restrictScalarsId'App_inv_apply

deleted theorem ModuleCat.restrictScalarsId'_hom_apply

deleted theorem ModuleCat.restrictScalarsId'_inv_apply