Def ModuleCat.image

Modification history

2026-09-04 11:59

Mathlib/Algebra/Category/ModuleCat/Images.lean

chore(CategoryTheory): use the new `↧` notation in concrete categories (#41811) …

Modified ModuleCat.image View on Github →

2023-05-26 09:02

Mathlib/Algebra/Category/ModuleCat/Images.lean

feat: port Algebra.Category.Module.Images (#4385)

Added ModuleCat.image View on Github →