mathlib
4b76b9d6
- chore(algebra/jordan/basic): remove unused imports (#15686)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(algebra/jordan/basic): remove unused imports (#15686) We don't need any linear algebra or the real numbers here
Author
eric-wieser
Parents
59382264
Loading