Structure CategoryTheory.AddGrp

Modification history

2026-04-03 08:22

Mathlib/CategoryTheory/Monoidal/Grp_.lean

feat(CategoryTheory/Monoidal): use `to_additive` for group objects (#37263)

Added CategoryTheory.AddGrp View on Github →