Bases and dimensionality of tensor products of modules #
These can not go into
linear_algebra.tensor_product since they depend on
linear_algebra.finsupp_vector_space which in turn imports
If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.
W are finite dimensional
K vector spaces, so is
V ⊗ W.