feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between MultilinearMap and DirectSum, and between PiTensorProduct and DirectSum

[smorel394]

This does three things:

• MultilinearMap.fromDirectSumEquiv (in LinearAlgebra/MultilinearMap/DirectSum.lean) calculates MultilinearMaps on a family of DirectSums. More precisely, if ι is a Fintype, if κ i is a family of types indexed by ι and we have a R-module M i j for every i : ι and j : κ i, this is the linear equivalence between Π p : (i : ι) → κ i, MultilinearMap R (fun i ↦ M i (p i)) M' and MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M'.
• PiTensorProduct.directSum (in LinearAlgebra/DirectSum/PiTensorProduct.lean): the distributivity property of a PiTensorProduct with respect to DirectSums in all its arguments.
• finsuppPiTensorProduct (in LinearAlgebra/DirectSum/Finsupp.lean): If ι is a Fintype, κ i is a family of types indexed by ι and M i is a family of R-modules indexed by ι, then the tensor product of the family κ i →₀ M i is linearly equivalent to ∏ i, κ i →₀ ⨂[R] i, M i.

• depends on: [Merged by Bors] - feat(LinearAlgebra/PiTensorProduct): some more functoriality properties of PiTensorProduct #11152
• depends on: [Merged by Bors] - feat(RingTheory/PiTensorProduct): extensionality and isomorphisms #11196

---

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(LinearAlgebra/PiTensorProduct): some more functoriality properties of PiTensorProduct #11152
• [Merged by Bors] - feat(RingTheory/PiTensorProduct): extensionality and isomorphisms #11196
  By Dependent Issues (🤖). Happy coding!