Theorem CategoryTheory.Grp.Hom.hom_one

Modification history

2026-04-09 16:23

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

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

Modified CategoryTheory.Grp.Hom.hom_one View on Github →

2025-11-08 15:24

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

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

Added CategoryTheory.Grp.Hom.hom_one View on Github →