rootForm_apply_apply — Mathlib

English

RootForm is the bilinear form on weights given by summing products of coroots: RootForm x y = ∑_i coroot'_i(x) · coroot'_i(y).

Русский

RootForm — билинеарная форма на весовом пространстве, задаваемая как сумма по i от произведений coroot'_i(x) и coroot'_i(y).

LaTeX

$$$ P.RootForm(x,y) = \\sum_i P.coroot' i(x) \\cdot P.coroot' i(y) $$$

Lean4

theorem rootForm_apply_apply (x y : M) : P.RootForm x y = ∑ i, P.coroot' i x * P.coroot' i y := by simp [RootForm]

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