Def ModuleCat.Hom.Simps.hom

Modification history

2025-01-27 16:24

Mathlib/Algebra/Category/ModuleCat/Basic.lean

feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) …

Added ModuleCat.Hom.Simps.hom View on Github →