Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tensor_product.direct_sum_left_tmul_lof

Modification history

2023-03-02 09:27
src/linear_algebra/direct_sum/tensor_product.lean
feat(linear_algebra/direct_sum/tensor_product): one-sided distributivity constructions (#18514) …
Added tensor_product.direct_sum_left_tmul_lofView on Github →