Commit 2023-03-31 10:15 fa99b800

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

added def TensorProduct.directSumLeft

added theorem TensorProduct.directSumLeft_symm_lof_tmul

added theorem TensorProduct.directSumLeft_tmul_lof

added def TensorProduct.directSumRight

added theorem TensorProduct.directSumRight_symm_lof_tmul

added theorem TensorProduct.directSumRight_tmul_lof

added theorem TensorProduct.directSum_lof_tmul_lof