bracket_tmul — Mathlib

English

The tensor-product Lie bracket is bilinear and compatible with the base ring, given on pure tensors by [s ⊗ x, t ⊗ y] = st ⊗ [x,y].

Русский

Скобка над тензором Ли является билинейной и согласуется с основанием, на простых тензорах: [s ⊗ x, t ⊗ y] = st ⊗ [x,y].

LaTeX

$$$⁅s \otimes x, t \otimes y⁆ = (s t) \otimes ⁅x,y⁆,$$$

Lean4

@[simp]
theorem bracket_tmul (s t : A) (x : L) (y : M) : ⁅s ⊗ₜ[R] x, t ⊗ₜ[R] y⁆ = (s * t) ⊗ₜ ⁅x, y⁆ :=
  rfl

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