Theorem ModuleCat.restrictScalarsIsoOfEquiv_inv_apply

Modification history

2026-04-19 10:51
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
chore(Algebra/Category): add `ModuleCat.restrictScalarsIsoOfEquiv` (#37773) …
Added ModuleCat.restrictScalarsIsoOfEquiv_inv_applyView on Github →