Theorem CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGen

Modification history

2026-01-12 11:29
Mathlib/CategoryTheory/MorphismProperty/Quotient.lean
feat(CategoryTheory): MorphismProperty induced on a quotient category (#33084) …
Added CategoryTheory.MorphismProperty.HasQuotient.iff_of_eqvGenView on Github →