e_lie_v_ne — Mathlib

English

If the root corresponding to j equals the root k plus the root i, then the bracket [e_k, v_i] equals (chainBotCoeff(k,i) + 1) times v_j.

Русский

Если корень j равен корню k плюс корень i, то скобка [e_k, v_i] равна (chainBotCoeff(k,i) + 1) множителю на v_j.

LaTeX

$$$\\text{If } \\mathrm{root}_j = \\mathrm{root}_k + \\mathrm{root}_i,\\\\ [e_k, v_i] = (\\mathrm{chainBotCoeff}(k,i) + 1) \\cdot v_j$$$

Lean4

theorem e_lie_v_ne {i j : ι} {k : b.support} (h : P.root j = P.root k + P.root i) :
    ⁅e k, v b i⁆ = (P.chainBotCoeff k i + 1 : R) • v b j :=
  by
  letI := P.indexNeg
  ext (l | l)
  · replace h : i ≠ -k := by rintro rfl; exact P.ne_zero j <| by simpa using h
    simp [e, h, -indexNeg_neg]
  · simp [e, ← h, Pi.single_apply]

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