Commit 2020-06-24 14:36 04a5bdbc

View on Github →

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.

Estimated changes

Modified src/data/finsupp.lean

added theorem finsupp.sum_smul_index'

Modified src/linear_algebra/basis.lean

added theorem module_equiv_finsupp_apply_basis

Modified src/linear_algebra/finsupp.lean

added theorem finsupp.coe_lsum

added theorem finsupp.dom_lcongr_single

added def finsupp.lcongr

added theorem finsupp.lcongr_single

modified def finsupp.lsum

modified theorem finsupp.lsum_apply

added theorem finsupp.lsum_single

added def finsupp_lequiv_direct_sum

added theorem finsupp_lequiv_direct_sum_single

added theorem finsupp_lequiv_direct_sum_symm_lof

added def finsupp_tensor_finsupp

added theorem finsupp_tensor_finsupp_single

added theorem finsupp_tensor_finsupp_symm_single

Modified src/linear_algebra/finsupp_vector_space.lean

added theorem finsupp.is_basis.tensor_product

modified theorem finsupp.is_basis_single

added theorem finsupp.is_basis_single_one

Modified src/linear_algebra/tensor_product.lean

added theorem tensor_product.congr_tmul

added theorem tensor_product.direct_sum_lof_tmul_lof