Theorem MonCat.forget_map

Modification history

2025-01-30 16:37
Mathlib/Algebra/Category/MonCat/Basic.lean
feat(Algebra/Category): concrete category refactor for `MonCat` (#21222) …
Modified MonCat.forget_mapView on Github →
2024-03-13 20:53
Mathlib/Algebra/Category/MonCat/Basic.lean
chore: remove more autoImplicit (#11336) …
Modified MonCat.forget_mapView on Github →
2023-05-18 20:51
Mathlib/Algebra/Category/MonCat/Basic.lean
feat: port Algebra.Category.Mon.Limits (#3073)
Modified MonCat.forget_mapView on Github →
2023-05-12 11:43
Mathlib/Algebra/Category/MonCat/Basic.lean
chore: refactor of concrete categories (#3900) …
Added MonCat.forget_mapView on Github →