# Tensor products of products #

This file shows that taking TensorProducts commutes with taking Prods in both arguments.

## Main results #

• TensorProduct.prodLeft
• TensorProduct.prodRight

## Notes #

See Mathlib.LinearAlgebra.TensorProduct.Pi for arbitrary products.

noncomputable def TensorProduct.prodRight (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] :
TensorProduct R M₁ (M₂ × M₃) ≃ₗ[R] TensorProduct R M₁ M₂ × TensorProduct R M₁ M₃

Tensor products distribute over a product on the right.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TensorProduct.prodRight_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) :
(TensorProduct.prodRight R M₁ M₂ M₃) (m₁ ⊗ₜ[R] (m₂, m₃)) = (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃)
@[simp]
theorem TensorProduct.prodRight_symm_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) :
(TensorProduct.prodRight R M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)
noncomputable def TensorProduct.prodLeft (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] :
TensorProduct R (M₁ × M₂) M₃ ≃ₗ[R] TensorProduct R M₁ M₃ × TensorProduct R M₂ M₃

Tensor products distribute over a product on the left .

Equations
Instances For
@[simp]
theorem TensorProduct.prodLeft_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) :
(TensorProduct.prodLeft R M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃)
@[simp]
theorem TensorProduct.prodLeft_symm_tmul (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃) [] [] [] [] [Module R M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) :
(TensorProduct.prodLeft R M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃