Inductive CategoryTheory.Groupoid.Free.redStep

Modification history

2025-10-03 14:43
Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
chore: replace CategoryTheory.FreeGroupoid with Quiver.FreeGroupoid (#30115) …
Deleted CategoryTheory.Groupoid.Free.redStepView on Github →
2023-05-18 07:49
Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
feat: port CategoryTheory.Groupoid.FreeGroupoid (#3347)
Added CategoryTheory.Groupoid.Free.redStepView on Github →