zero_le_posForm — Mathlib

English

For any x in the span of the roots, the bilinear form posRootForm S applied to (x,x) is nonnegative.

Русский

Для любого вектора x из линейной оболочки корней форма-билинейная posRootForm S на (x,x) неотрицательна.

LaTeX

$$$ 0 \le (P.posRootForm S).posForm x x $$$

Lean4

theorem zero_le_posForm (x : span S (range P.root)) : 0 ≤ (P.posRootForm S).posForm x x :=
  by
  obtain ⟨s, _, hs⟩ := P.exists_ge_zero_eq_rootForm S x.1 x.2
  have : s = (P.posRootForm S).posForm x x :=
    FaithfulSMul.algebraMap_injective S R <| (P.algebraMap_posRootForm_posForm S x x) ▸ hs
  rwa [← this]

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