Commit 2023-09-18 15:32 a150006e

View on Github →

feat(LinearAlgebra/TensorProduct/Prod): TensorProduct distributes over Prod (#7226) As requested over a year ago by @kbuzzard.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/TensorProduct/Prod.lean

added def TensorProduct.prodLeft

added theorem TensorProduct.prodLeft_symm_tmul

added theorem TensorProduct.prodLeft_tmul

added def TensorProduct.prodRight

added theorem TensorProduct.prodRight_symm_tmul

added theorem TensorProduct.prodRight_tmul