mul_apply — Mathlib

English

The multiplication of simple tensors distributes componentwise: (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 mul_apply (a₁ a₂ : A) (b₁ b₂ : B) : mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) :=
  rfl

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