feat(linear_algebra/pi_tensor_product): tmul distributes over tprod (#6126)
feat(linear_algebra/pi_tensor_product): tmul distributes over tprod (#6126)

This adds the equivalence `(⨂[R] i : ι, M) ⊗[R] (⨂[R] i : ι₂, M) ≃ₗ[R] ⨂[R] i : ι ⊕ ι₂, M`.
Working with dependently-typed `M` here is more trouble than it's worth, as we don't have any typeclass structures on `sum.elim M N` right now,

This is one of the pieces needed to provide a ring structure on `⨁ n, ⨂[R] i : fin n, M`, but that's left for another time.





leanprover-community/mathlib,leanprover-community/mathlib