English
Define adF-relations for Cartan matrix A by taking ad(F_i) raised to the (−A_{ij}).toNat power acting on [F_i, F_j].
Русский
Задаются adF-реляции: действие ad(F_i) на скаляр (-A_{ij}).toNat степень на братике [F_i, F_j].
LaTeX
$$$adF(R) : B\\times B \\to FreeLieAlgebra R(Generators B) = uncurry(\\lambda i j, ad(F_i)^{(-A_{ij}).toNat}([F_i, F_j]))$$$
Lean4
/-- The terms corresponding to the `⁅H, F⁆`-relations. -/
def HF : B × B → FreeLieAlgebra R (Generators B) :=
uncurry fun i j => ⁅H i, F j⁆ + A i j • F j