mathlib
51f80a3f
- feat(data/quot): quotient.ind' (#691)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
feat(data/quot): quotient.ind' (#691) * feat(data/quot): quotient.ind' * correct elaborator tag; theorems not definitions
References
#691 - feat(data/quot): quotient.ind'
Author
kbuzzard
Committer
ChrisHughes24
Parents
9615b385
Loading