hasBracketAux — Mathlib

English

The Lie bracket on a tensor product satisfies a Leibniz-type rule in the right argument: ⁅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

/-- It is useful to define the bracket via this auxiliary function so that we have a type-theoretic
expression of the fact that `L` acts by linear endomorphisms. It simplifies the proofs in
`lieRingModule` below. -/
def hasBracketAux (x : L) : Module.End R (M ⊗[R] N) :=
  (toEnd R L M x).rTensor N + (toEnd R L N x).lTensor M

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