Commit 2024-04-08 20:05 69bf34c2
View on Github →feat(Mathlib/LinearAlgebra/DirectSum/Finsupp): tensor products of finsupp sums (#11635)
Modules
TensorProduct.finsuppLeft
, the tensor product ofι →₀ M
andN
is linearly equivalent toι →₀ M ⊗[R] N
TensorProduct.finsuppScalarLeft
, the tensor product ofι →₀ R
andN
is linearly equivalent toι →₀ N
TensorProduct.finsuppRight
, the tensor product ofM
andι →₀ N
is linearly equivalent toι →₀ M ⊗[R] N
TensorProduct.finsuppLeft'
, ifM
is anS
-module, then the tensor product ofι →₀ M
andN
isS
-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.