rootForm_self_sum_of_squares — Mathlib

English

For any j in ι, RootForm evaluated at (root j, root j) equals the sum of squares of the pairings: RootForm(root j, root j) = ∑_i (pairing j i)^2.

Русский

Для любого j в ι значение RootForm на (root j, root j) равно сумме квадратов парировок: RootForm(root j, root j) = ∑_i (pairing j i)^2.

LaTeX

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

Lean4

theorem rootForm_self_sum_of_squares (x : M) : IsSumSq (P.RootForm x x) :=
  P.rootForm_apply_apply x x ▸ IsSumSq.sum_mul_self Finset.univ _

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