Theorem CategoryTheory.Quotient.comp_left

Modification history

2026-01-12 11:29
Mathlib/CategoryTheory/Quotient.lean
feat(CategoryTheory): MorphismProperty induced on a quotient category (#33084) …
Deleted CategoryTheory.Quotient.comp_leftView on Github →
2023-03-02 07:55
Mathlib/CategoryTheory/Quotient.lean
feat: port CategoryTheory.Quotient (#2339)
Added CategoryTheory.Quotient.comp_leftView on Github →