Commit 2023-03-02 07:55 062aacd0

View on Github →

feat: port CategoryTheory.Quotient (#2339)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Quotient.lean

added theorem CategoryTheory.Quotient.CompClosure.of

added inductive CategoryTheory.Quotient.CompClosure

added def CategoryTheory.Quotient.Hom

added def CategoryTheory.Quotient.comp

added theorem CategoryTheory.Quotient.comp_left

added theorem CategoryTheory.Quotient.comp_mk

added theorem CategoryTheory.Quotient.comp_right

added def CategoryTheory.Quotient.functor

added theorem CategoryTheory.Quotient.functor_map_eq_iff

added def CategoryTheory.Quotient.lift.isLift

added theorem CategoryTheory.Quotient.lift.isLift_hom

added theorem CategoryTheory.Quotient.lift.isLift_inv

added def CategoryTheory.Quotient.lift

added theorem CategoryTheory.Quotient.lift_map_functor_map

added theorem CategoryTheory.Quotient.lift_spec

added theorem CategoryTheory.Quotient.lift_unique

added structure CategoryTheory.Quotient

added def HomRel