rootForm_root_self — Mathlib

English

A variant of the self-pairing formula: RootForm root j with itself equals the sum of squares of the pairings with all roots.

Русский

Вариант формулы самопарирования: RootForm(root j, root j) равно сумме квадратов парирований с всеми корнями.

LaTeX

$$$ P.RootForm(P.root(j), P.root(j)) = \\sum_i (P.pairing(j,i))^2 $$$

Lean4

theorem rootForm_root_self (j : ι) : P.RootForm (P.root j) (P.root j) = ∑ (i : ι), (P.pairing j i) * (P.pairing j i) :=
  by simp [rootForm_apply_apply]

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