Theorem RingHom.toModule_smul

Modification history

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