tmul_mul_tmul — Mathlib

English

The product of two simple tensors equals the simple tensor of the products: (a1 ⊗ b1) · (a2 ⊗ b2) = (a1 a2) ⊗ (b1 b2).

Русский

Произведение двух простых тензоров равно простому тензору произведений: (a1 ⊗ b1) · (a2 ⊗ b2) = (a1 a2) ⊗ (b1 b2).

LaTeX

$$$ (a_1 \otimes_R b_1) \cdot (a_2 \otimes_R b_2) = (a_1 a_2) \otimes_R (b_1 b_2) $$$

Lean4

@[simp]
theorem tmul_mul_tmul (a₁ a₂ : A) (b₁ b₂ : B) : a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) :=
  rfl

Похожие утверждения