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

[AntoineChambert-Loir]

trafficstars

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.

---

[acmepjz]

Thank you very much! It looks good for me.

[AntoineChambert-Loir]

!bench

[leanprover-bot]

Here are the benchmark results for commit b400dac8f756ca9b992ef57fbf3d6e5dbb2cb54e. There were significant changes against commit f4fd1b19f0e2ab3989c2fef5511ab2341f8b2607:

  Benchmark                                  Metric         Change
  ================================================================
- ~Mathlib.LinearAlgebra.DirectSum.Finsupp   instructions   244.6%

[AntoineChambert-Loir]

@alreadydone, is there something else that you would want me to add or change?

[AntoineChambert-Loir]

Thanks for the shorter versions, I'll use them, and I'm OK to make the arguments of finsuppLeft explicit, in accordance with what is done for docs#TensorProduct.directSumLeft

[alreadydone]

Can you please fix the compile errors (which probably results from the implicitness changes)? Thanks!

[AntoineChambert-Loir]

I had not noticed that there were errors left, sorry. I make the necessary adjustments at once.

[alreadydone]

Thanks 🎉 maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[ocfnash]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style