mathlib3
Rename Groupoid.lean to groupoid_category.lean
#1353
Merged
Overview
Commits
1
Changes
View On GitHub

Rename Groupoid.lean to groupoid_category.lean #1353

ChrisHughes24 merged 1 commit into master from ChrisHughes24-patch-2
ChrisHughes24
ChrisHughes24 Rename Groupoid.lean to groupoid_category.lean
50987164
ChrisHughes24 ChrisHughes24 requested a review 6 years ago
ChrisHughes24 ChrisHughes24 merged a489719b into master 6 years ago
ChrisHughes24 ChrisHughes24 deleted the ChrisHughes24-patch-2 branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum