Commit 2023-05-03 01:24 77aa05d8

View on Github →

feat: port CategoryTheory.Category.Groupoid (#3761)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/Grpd.lean

added theorem CategoryTheory.Grpd.coe_of

added def CategoryTheory.Grpd.forgetToCat

added theorem CategoryTheory.Grpd.hom_to_functor

added theorem CategoryTheory.Grpd.id_to_functor

added def CategoryTheory.Grpd.objects

added def CategoryTheory.Grpd.of

added theorem CategoryTheory.Grpd.piIsoPi_hom_π

added def CategoryTheory.Grpd.piLimitFan

added def CategoryTheory.Grpd.piLimitFanIsLimit

added def CategoryTheory.Grpd