Commit 2019-12-15 16:39 9a37e3fd
View on Github →refactor(*): make vector_space an abbreviation for module (#1793)
- refactor(*): make vector_space an abbreviation for module
- Remove superfluous instances
- Fix build
- Add Note[vector space definition]
- Update src/algebra/module.lean
- Fix build (hopefully)
- Update src/measure_theory/bochner_integration.lean