f_lie_v_ne — Mathlib

English

If the root i equals the sum of roots j and k, then the bracket [f_k, v_i] equals (chainTopCoeff(k,i) + 1) times v_j.

Русский

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

LaTeX

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

Lean4

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

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