English
Tensor products distribute over a product on the left: (M1 × M2) ⊗_R M3 ≃_l[S] (M1 ⊗_R M3) × (M2 ⊗_R M3).
Русский
Тензорные произведения распределяются по левой части над произведением: (M1 × M2) ⊗_R M3 ≃ (M1 ⊗_R M3) × (M2 ⊗_R M3).
LaTeX
$$$ (M_1 \\times M_2) \\otimes_R M_3 \\cong (M_1 \\otimes_R M_3) \\times (M_2 \\otimes_R M_3) $$$
Lean4
/-- Tensor products distribute over a product on the left . -/
def prodLeft : (M₁ × M₂) ⊗[R] M₃ ≃ₗ[S] (M₁ ⊗[R] M₃) × (M₂ ⊗[R] M₃) :=
AddEquiv.toLinearEquiv
(TensorProduct.comm _ _ _ ≪≫ₗ TensorProduct.prodRight R R _ _ _ ≪≫ₗ
(TensorProduct.comm R _ _).prodCongr (TensorProduct.comm R _ _)).toAddEquiv
fun c x ↦ x.induction_on (by simp) (by simp [TensorProduct.smul_tmul']) (by simp_all)
