Mathlib v3 is deprecated. Go to Mathlib v4

Theorem AddCommGroup.has_limit.lift_apply

Modification history

2022-05-20 00:16

src/algebra/category/Group/biproducts.lean

refactor(category_theory/discrete): make discrete irreducible (#13762)

Deleted AddCommGroup.has_limit.lift_apply View on Github →

2020-04-12 20:36

src/algebra/category/Group/biproducts.lean

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

Added AddCommGroup.has_limit.lift_apply View on Github →