mathlib

8b59d97d - 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.