Def CategoryTheory.ModuleCat.RestrictScalars.map'

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.map'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.map'View on Github →