corootForm_apply_apply — Mathlib

English

CorootForm x y is given by summing products of root values: CorootForm x y = ∑_i root'_i(x) · root'_i(y).

Русский

CorootForm x y задается как сумма по i произведений значений корня: CorootForm x y = ∑_i root'_i(x) · root'_i(y).

LaTeX

$$$ P.CorootForm(x,y) = \\sum_i P.root' i(x) \\cdot P.root' i(y) $$$

Lean4

theorem corootForm_apply_apply (x y : N) : P.CorootForm x y = ∑ i, P.root' i x * P.root' i y :=
  P.flip.rootForm_apply_apply x y

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