Theorem IsCommMon.ofRepresentableBy

Modification history

2025-05-11 10:35
Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean
feat: Yoneda for (comm) group objects (#24118) …
Modified IsCommMon.ofRepresentableByView on Github →
2025-05-07 21:03
Mathlib/CategoryTheory/Monoidal/Yoneda.lean
refactor(CategoryTheory): Make `ChosenFiniteProducts` extend `MonoidalCategory` (#24399) …
Modified IsCommMon.ofRepresentableByView on Github →
2025-03-09 16:57
Mathlib/CategoryTheory/Monoidal/Yoneda.lean
feat: objects representing functors to `CommMon` satisfy `IsCommMon` (#22700) …
Added IsCommMon.ofRepresentableByView on Github →