Commit 2024-04-08 20:05 69bf34c2

feat(Mathlib/LinearAlgebra/DirectSum/Finsupp): tensor products of finsupp sums (#11635)

Modules

• TensorProduct.finsuppLeft, the tensor product of ι →₀ M and N is linearly equivalent to ι →₀ M ⊗[R] N
• TensorProduct.finsuppScalarLeft, the tensor product of ι →₀ R and N is linearly equivalent to ι →₀ N
• TensorProduct.finsuppRight, the tensor product of M and ι →₀ N is linearly equivalent to ι →₀ M ⊗[R] N
• TensorProduct.finsuppLeft', if M is an S-module, then the tensor product of ι →₀ M and N is S-linearly equivalent to ι →₀ M ⊗[R] N This is the first part of PR #10824 which contains three applications of these functions to monoid algebras, polynomials and multivariate polynomials. It has been split because this part is reasonably sound, while the three other files are more like propositions.