Commit 2020-05-18 13:38 4026bd8c
View on Github →feat(category_theory/full_subcategory): induced category from a groupoid is a groupoid (#2715) Also some minor cleanup to the same file.
feat(category_theory/full_subcategory): induced category from a groupoid is a groupoid (#2715) Also some minor cleanup to the same file.