EF — Mathlib · SciLib

English

Define the EF-relations for a Cartan matrix A: it assigns to a pair (i,j) the Lie expression either [E_i, F_i] − A_{ij} F_j (for i=j) or [E_i, F_j] (for i≠j).

Русский

Задаются EF-отношения для Картановой матрицы A: для пары (i,j) выражение в Ли-алгебре равно [E_i, F_i] − A_{ij} F_j при i=j и [E_i, F_j] при i≠j.

LaTeX

$$$EF(R) : B\\times B \\to FreeLieAlgebra R(Generators B)$ как uncurry\\; (\\lambda i j, [H_i, E_j] \\text{ или } [E_i, F_j] \\text{ с модификацией})$$$

Lean4

/-- The terms corresponding to the `⁅E, F⁆`-relations. -/
def EF [DecidableEq B] : B × B → FreeLieAlgebra R (Generators B) :=
  uncurry fun i j => if i = j then ⁅E i, F i⁆ - H i else ⁅E i, F j⁆

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