Def TensorProduct.directSumLeft

Modification history

2026-01-21 06:56

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

feat(LinearAlgebra): make TensorProduct.finsuppLeft and friends heterobasic (#33469)

Modified TensorProduct.directSumLeft View on Github →

2023-03-31 10:15

Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

feat: port LinearAlgebra.DirectSum.TensorProduct (#2977)

Added TensorProduct.directSumLeft View on Github →