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

[smorel394]

trafficstars

This does three things:

• MultilinearMap.fromDirectSumEquiv (in LinearAlgebra/MultilinearMap/DirectSum.lean) calculates MultilinearMaps on a family of DirectSums. More precisely, if 'ιis aFintype, if κ iis a family of types indexed byιand we have aR-module M i jfor everyi : ιandj : κ i, this is the linear equivalence between Π p : (i : ι) → κ i, MultilinearMap R (fun i ↦ M i (p i)) M'andMultilinearMap 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.

• [x] depends on: #11152
• [x] depends on: #11196

---