Theorem CategoryTheory.ModuleCat.ExtendScalars.map'_id

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

2023-07-07 06:10

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

feat: port Algebra.Category.Module.ChangeOfRings (#4300)

Added CategoryTheory.ModuleCat.ExtendScalars.map'_id View on Github →