Theorem CategoryTheory.Mon.Hom.hom_mul

Modification history

2026-03-27 18:43

Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

feat(CategoryTheory/Monoidal): use to_additive for the Yoneda embedding of monoid objects (#37265)

Modified CategoryTheory.Mon.Hom.hom_mul View on Github →

2025-11-08 15:24

Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

feat: commutative monoids are internal monoids (#29765) …

Added CategoryTheory.Mon.Hom.hom_mul View on Github →