Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-06 07:11 62e7d353

View on Github →

feat(category_theory/limits): uniqueness of preadditive structures (#12342)

Estimated changes

Modified src/category_theory/abelian/non_preadditive.lean

Modified src/category_theory/limits/shapes/biproducts.lean

modified theorem category_theory.limits.bicone_ι_π_self

added theorem category_theory.limits.biprod.add_eq_lift_desc_id

added theorem category_theory.limits.biprod.add_eq_lift_id_desc