mathlib3
338bbd20
- chore(measure/theory): remove useless module instances (#3031)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(measure/theory): remove useless module instances (#3031) Remove useless `module` and `vector_space` instances, as these words are now synonyms of `semimodule`. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
sgouezel
Parents
593f731d
Loading