Library
▹
Linear algebra
▹
Vector spaces
Definition 3.1.1.
Let
F
be a
field
. We define:
Vec
(
F
)
:
=
LMod
(
F
)
We write “let
V
be a vector space over
F
” for “let
V
∈
Vec
(
F
).”
Remarks.
For vector spaces, we reuse the definitions related to modules over a ring where applicable.
References.
https://en.wikipedia.org/wiki/Vector_space
https://mathworld.wolfram.com/VectorSpace.html
https://proofwiki.org/wiki/Definition:Vector_Space
https://ncatlab.org/nlab/show/vector+space
https://leanprover-community.github.io/mathlib_docs/algebra/module/basic.html#vector_space