Def ModuleCat.asHom

Modification history

2024-12-03 14:22

Mathlib/Algebra/Category/ModuleCat/Basic.lean

chore(Algebra/Category/ModuleCat): rename `ModuleCat.asHom` to `ModuleCat.ofHom` (#19705) …

Deleted ModuleCat.asHom View on Github →

2023-04-11 12:30

Mathlib/Algebra/Category/ModuleCat/Basic.lean

feat: port Algebra.Category.Module.Basic (#3260)

Added ModuleCat.asHom View on Github →