Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.exact.lift_comp

Modification history

2021-05-15 08:16
src/category_theory/preadditive/projective.lean
feat(category_theory/*/projective): refactor treatment of projective objects (#7485)
Added category_theory.exact.lift_compView on Github →