mathlib
04a5bdbc - feat(linear_algebra/finsupp_vector_space): is_basis.tensor_product (#3147)

Commit

5 years ago

feat(linear_algebra/finsupp_vector_space): is_basis.tensor_product (#3147) If `b : ι → M` and `c : κ → N` are bases then so is `λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N`.

Author

kckennylau

Parents

dd9b5c68

mathlib 04a5bdbc - feat(linear_algebra/finsupp_vector_space): is_basis.tensor_product (#3147)

mathlib
04a5bdbc - feat(linear_algebra/finsupp_vector_space): is_basis.tensor_product (#3147)