mathlib

ef4d2354 - feat(category_theory): biproducts, and biproducts in AddCommGroup (#2187)

feat(category_theory): biproducts, and biproducts in AddCommGroup (#2187) This PR 1. adds typeclasses `has_biproducts` (implicitly restricting to finite biproducts, which is the only interesting case) and `has_binary_biproducts`, and the usual tooling for special shapes of limits. 2. provides customised `has_products` and `has_coproducts` instances for `AddCommGroup`, which are both just dependent functions (for `has_coproducts` we have to assume the indexed type is finite and decidable) 3. because these custom instances have identical underlying objects, it's trivial to put them together to get a `has_biproducts AddCommGroup`. 4. as for 2 & 3 with binary biproducts for AddCommGroup, implemented simply as the cartesian group.