Def CategoryTheory.Preadditive.toCommGrp

Modification history

2025-10-16 01:23
Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
chore: rename `Grp_` to `Grp` (#30496) …
Modified CategoryTheory.Preadditive.toCommGrpView on Github →
2025-02-20 11:46
Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
feat: commutative group objects in additive categories (#21521)
Added CategoryTheory.Preadditive.toCommGrpView on Github →