Linear structures on function with finite support
ι →₀ M #
This file contains results on the
R-module structure on functions of finite support from a type
ι to an
M, in particular in the case that
R is a field.
Furthermore, it contains some facts about isomorphisms of vector spaces from equality of dimension as well as the cardinality of finite dimensional vector spaces.
Move the second half of this file to more appropriate other files.
If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.
K-vector spaces are equivalent if their dimension is the same.