Mathlib v3 is deprecated. Go to Mathlib v4

Def tensor_product.direct_sum_left

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_leftView on Github →