Theorem CategoryTheory.ModuleCat.restrictScalars.smul_def'

Modification history

2023-09-08 11:01
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
feat(Algebra/Category/ModuleCat): composition of restriction of scalar functors (#6915) …
Deleted CategoryTheory.ModuleCat.restrictScalars.smul_def'View on Github →
2023-07-07 06:10
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
feat: port Algebra.Category.Module.ChangeOfRings (#4300)
Added CategoryTheory.ModuleCat.restrictScalars.smul_def'View on Github →