Commit 2023-05-18 07:49 0d5e1c84

View on Github →

feat: port CategoryTheory.Groupoid.FreeGroupoid (#3347)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

added def CategoryTheory.FreeGroupoid

added theorem CategoryTheory.Groupoid.Free.congr_comp_reverse

added theorem CategoryTheory.Groupoid.Free.congr_reverse

added theorem CategoryTheory.Groupoid.Free.congr_reverse_comp

added theorem CategoryTheory.Groupoid.Free.freeGroupoidFunctor_comp

added theorem CategoryTheory.Groupoid.Free.freeGroupoidFunctor_id

added def CategoryTheory.Groupoid.Free.lift

added theorem CategoryTheory.Groupoid.Free.lift_spec

added theorem CategoryTheory.Groupoid.Free.lift_unique

added def CategoryTheory.Groupoid.Free.of

added theorem CategoryTheory.Groupoid.Free.of_eq

added def CategoryTheory.Groupoid.Free.quotInv

added inductive CategoryTheory.Groupoid.Free.redStep

added def CategoryTheory.freeGroupoidFunctor