mathlib3
feat(data/quot): quotient.ind'
#691
Merged
Overview
Commits
2
Changes
View On GitHub

feat(data/quot): quotient.ind' #691

ChrisHughes24 merged 2 commits into master from kmb_quotient
kbuzzard
kbuzzard feat(data/quot): quotient.ind'
d8439d64
ChrisHughes24
ChrisHughes24 commented on 2019-02-06
kbuzzard correct elaborator tag; theorems not definitions
b15be278
ChrisHughes24 ChrisHughes24 merged 51f80a3f into master 7 years ago
kbuzzard kbuzzard deleted the kmb_quotient branch 7 years ago

Login to write a write a comment.

Login via GitHub

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