Commit 2023-02-15 08:00 86092397

View on Github →

feat: port CategoryTheory.Groupoid (#2282)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Groupoid.lean

added def CategoryTheory.Groupoid.invEquiv

added theorem CategoryTheory.Groupoid.inv_eq_inv

added def CategoryTheory.Groupoid.isoEquivHom

added def CategoryTheory.Groupoid.ofHomUnique

added theorem CategoryTheory.Groupoid.reverse_eq_inv