mathlib
ce48b6ba
- chore(data/finsupp): drop `finsupp.module` and `vector_space` (#3009)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(data/finsupp): drop `finsupp.module` and `vector_space` (#3009) These instances are not needed as `module` and `vector_space` are abbreviations for `semimodule`. Also add two bundled versions of `eval`: as `add_monoid_hom` and as `linear_map`.
Author
urkud
Parents
cf0c6b83
Loading