Theorem ModuleCat.extendScalarsId_hom_app_one_tmul

Modification history

2024-12-20 15:50
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules (#18197) …
Added ModuleCat.extendScalarsId_hom_app_one_tmulView on Github →