posRootForm_posForm_apply_apply — Mathlib

English

Let P be a RootPairing and S a suitable ordered ring; for all x,y in the root span S, the posRootForm applied to x and y is the finite sum over the index i of the i-th coroot evaluated at x and y.

Русский

Пусть P — корневое соответствие, S — подходящее упорядоченное кольцо; для всех x,y из span корней S, posRootForm применяется к x и y и равен конечно-сумме по индексу i от значений coroot_i(x)·coroot_i(y).

LaTeX

$$$ (P.posRootForm\ S).posForm\\ x\\ y = \\sum_{i} P.coroot'In\\ S\\ i\\ x \\cdot P.coroot'In\\ S\\ i\\ y $$$

Lean4

theorem posRootForm_posForm_apply_apply (x y : P.rootSpan S) :
    (P.posRootForm S).posForm x y = ∑ i, P.coroot'In S i x * P.coroot'In S i y :=
  by
  refine (FaithfulSMul.algebraMap_injective S R) ?_
  simp [posRootForm, rootForm_apply_apply]

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