Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.idempotents.karoubi.decomposition

Modification history

2022-03-01 02:55

src/category_theory/idempotents/biproducts.lean

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

Added category_theory.idempotents.karoubi.decomposition View on Github →