Def tensor_product.direct_sum
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) …
Deleted tensor_product.direct_sumView on Github →2020-07-21 07:47
src/linear_algebra/direct_sum/tensor_product.lean
refactor(linear_algebra/*): postpone importing material on direct sums (#3484) …
Modified tensor_product.direct_sumView on Github →2019-10-10 11:14
src/linear_algebra/tensor_product.lean
chore(linear_algebra): rename type variables (#1521) …
Modified tensor_product.direct_sumView on Github →2019-01-28 19:59
src/linear_algebra/tensor_product.lean
feat(*) refactor module
Modified tensor_product.direct_sumView on Github →