Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 02:55 37885e8c

View on Github →

feat(category_theory/idempotents): biproducts in idempotent completions (#12333)

Estimated changes

Created src/category_theory/idempotents/biproducts.lean

added def category_theory.idempotents.karoubi.biproducts.bicone

added def category_theory.idempotents.karoubi.complement

added def category_theory.idempotents.karoubi.decomposition

added theorem category_theory.idempotents.karoubi.karoubi_has_finite_biproducts