Lean Mathlib
Posted on August 2, 2019
Tags: lean
journal in exploring mathlib
1 vector space aka module
- Module R M
- [Scalar semi-ring R] - \(S(+,\cdot)\) typical addition and multiplication
- represents scalar multiplication of vectors
- [additive communitive monoid M] - basically a monoid that is also communitive
- represents linear combination of vectors
- [Scalar semi-ring R] - \(S(+,\cdot)\) typical addition and multiplication
A module is a generalization of vector spaces to a scalar semiring
2 Subspace aka submodule
- Subspace R M
- division ring R
- additive communitative group M
3 Tropical algebra
- remember semi-ring \(S(+,\cdot)\) is just typical add,multiply
- replace that with \(S(min,+)\)