Theorem CategoryTheory.Quotient.compClosure_eq_self

Modification history

2026-01-12 11:29
Mathlib/CategoryTheory/Quotient.lean
feat(CategoryTheory): MorphismProperty induced on a quotient category (#33084) …
Deleted CategoryTheory.Quotient.compClosure_eq_selfView on Github →
2023-09-15 10:01
Mathlib/CategoryTheory/Quotient.lean
feat: the quotient category is preadditive (#7049) …
Added CategoryTheory.Quotient.compClosure_eq_selfView on Github →