lie_tmul_right — Mathlib

English

Reiteration of the right-tensor bracket identity for the tensor product: ⁅x, m ⊗ n⁆ = ⁅x, m⁆ ⊗ n + m ⊗ ⁅x, n⁆.

Русский

Повторное утверждение формулы лейбница для правого тензорного произведения: ⁅x, m ⊗ n⁆ = ⁅x, m⁆ ⊗ n + m ⊗ ⁅x, n⁆.

LaTeX

$$$\,[x, m \otimes n\!] = [x,m] \otimes n + m \otimes [x,n]$$$

Lean4

@[simp]
theorem lie_tmul_right (x : L) (m : M) (n : N) : ⁅x, m ⊗ₜ[R] n⁆ = ⁅x, m⁆ ⊗ₜ n + m ⊗ₜ ⁅x, n⁆ :=
  show hasBracketAux x (m ⊗ₜ[R] n) = _ by
    simp only [hasBracketAux, LinearMap.rTensor_tmul, toEnd_apply_apply, LinearMap.add_apply, LinearMap.lTensor_tmul]

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