HE — Mathlib · SciLib

English

Define HF-relations for the Cartan matrix A by pairing H_i and F_j with the relation ad(H_i) acting on F_j scaled by A_{ij}.

Русский

Задаются HF-реляции для Картановой матрицы A через пары H_i, F_j с действием ad(H_i) на F_j, масштабированным коэффициентами A_{ij}.

LaTeX

$$$HF(R) : B\\times B \\to FreeLieAlgebra R(Generators B)$ равняется uncurry\\; (\\lambda i j, [H_i, F_j] - A_{ij}\\cdot F_j)$$$

Lean4

/-- The terms corresponding to the `⁅H, E⁆`-relations. -/
def HE : B × B → FreeLieAlgebra R (Generators B) :=
  uncurry fun i j => ⁅H i, E j⁆ - A i j • E j

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