adF — Mathlib

English

Equality of the adE relation with its Lie-algebra expression for Cartan data, matching the general adE construction.

Русский

Согласование adE с его выражением в Ли-алгебре для Картановой матрицы.

LaTeX

$$$CartanMatrix.Relations.adE\\;R\\;A = (\\lambda i j, ad(E_i)^{(-A_{ij}).toNat}([E_i,E_j]))$$$

Lean4

/-- The terms corresponding to the `ad F`-relations.

See also `adE` docstring. -/
def adF : B × B → FreeLieAlgebra R (Generators B) :=
  uncurry fun i j => ad (F i) ^ (-A i j).toNat <| ⁅F i, F j⁆

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