Commit 2025-02-20 11:46 ab742a3f

View on Github →

feat: commutative group objects in additive categories (#21521)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/CommGrp_.lean

added def CategoryTheory.Preadditive.commGrpEquivalence

added def CategoryTheory.Preadditive.commGrpEquivalenceAux

added def CategoryTheory.Preadditive.toCommGrp