Def CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts

Modification history

2024-03-09 09:32
Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
refactor: do not allow `nsmul` and `zsmul` to default automatically (#6262) …
Modified CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproductsView on Github →
2023-03-17 12:26
Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
feat: port CategoryTheory.Preadditive.OfBiproducts (#2939)
Added CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproductsView on Github →