Commit 2024-11-14 06:25 9380e7b9

View on Github →

feat(Algebra/TensorProduct): tensor product commutes with finite products (#18635)

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem TensorProduct.single_tmul

added theorem TensorProduct.tmul_single

Modified Mathlib/LinearAlgebra/TensorProduct/Pi.lean

added theorem TensorProduct.piRightHom_tmul

added def TensorProduct.piRightInv

added theorem TensorProduct.piRight_apply

added theorem TensorProduct.piRight_symm_apply

added theorem TensorProduct.piRight_symm_single