English
Equivalence of adF definitions: the adF-relations equal the explicit polynomially defined Lie expressions in the Cartan setup.
Русский
Эквивалентность определений adF: adF-реляции равны явным выражениям Ли в настройке Кардана.
LaTeX
$$$CartanMatrix.Relations.adF\\;R\\;A = (\\lambda i j, [F_i,F_j]^{(-A_{ij}).toNat})$$$
Lean4
/-- The terms corresponding to the `ad E`-relations.
Note that we use `Int.toNat` so that we can take the power and that we do not bother
restricting to the case `i ≠ j` since these relations are zero anyway. We also defensively
ensure this with `adE_of_eq_eq_zero`. -/
def adE : B × B → FreeLieAlgebra R (Generators B) :=
uncurry fun i j => ad (E i) ^ (-A i j).toNat <| ⁅E i, E j⁆
