mathlib

9b9d125b - feat(linear_algebra/direct_sum/tensor_product): one-sided distributivity constructions (#18514)

feat(linear_algebra/direct_sum/tensor_product): one-sided distributivity constructions (#18514) We had the two-sided distributivity already, analogous to `finset.sum_mul_sum`. This PR adds constructions analogous to `finset.mul_sum` and `finset.sum_mul`. This also tidies some namespacing and explicitness issues.