Commit 2023-03-02 09:27 9b9d125b

View on Github →

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.

Estimated changes

Modified src/linear_algebra/direct_sum/finsupp.lean

Modified src/linear_algebra/direct_sum/tensor_product.lean

deleted def tensor_product.direct_sum

added def tensor_product.direct_sum_left

added theorem tensor_product.direct_sum_left_symm_lof_tmul

added theorem tensor_product.direct_sum_left_tmul_lof

added def tensor_product.direct_sum_right

added theorem tensor_product.direct_sum_right_symm_lof_tmul

added theorem tensor_product.direct_sum_right_tmul_lof