mathlib
7e39766e
- chore(topology/algebra/module/basic): golf using injective APIs
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(topology/algebra/module/basic): golf using injective APIs This requires the `has_scalar` instance to be moved up from further down the file.
References
#12676 - chore(topology/algebra/module/basic): golf using injective APIs
Author
eric-wieser
Committer
eric-wieser
Parents
fc882ff8
Loading
