rootSpaceProduct_def — Mathlib

English

The root space product sends a pair of root vectors to their Lie bracket in L, via a weight-sum relationship.

Русский

Произведение корневого пространства отправляет пару корневых векторов в их скобку в L, с учётом сумма весов.

LaTeX

$$$\text{rootSpaceProduct}\; R L H χ_1 χ_2 χ_3 hχ (x\otimes y) = [x,y]$$$

Lean4

@[simp]
theorem rootSpaceProduct_def : rootSpaceProduct R L H = rootSpaceWeightSpaceProduct R L H L :=
  rfl

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