Theorem CategoryTheory.exists_colimitsOfShape_splitMonomorphisms_of_isCardinalPure

Modification history

2026-09-25 12:29
Mathlib/CategoryTheory/Presentable/CardinalPure.lean
feat(CategoryTheory): pure morphisms are filtered colimits of split monomorphisms (#44044) …
Added CategoryTheory.exists_colimitsOfShape_splitMonomorphisms_of_isCardinalPureView on Github →