mathlib3
4026bd8c - feat(category_theory/full_subcategory): induced category from a groupoid is a groupoid (#2715)

Commit

6 years ago

feat(category_theory/full_subcategory): induced category from a groupoid is a groupoid (#2715) Also some minor cleanup to the same file.

Author

rwbarton

Parents