eval_eq — Mathlib

English

For X : σ → R and f ∈ MvPolynomial σ R, evaluation equals the coefficient-sum formula: eval X f = ∑ d ∈ supp(f) coeff(f,d) · ∏ i ∈ supp(d) X_i^{d(i)}.

Русский

Для X : σ → R и f ∈ MvPolynomial σ R формула вычисления: eval X f = ∑ d ∈ supp(f) coeff(f,d) · ∏ i ∈ supp(d) X_i^{d(i)}.

LaTeX

$$$\\mathrm{eval}\\ X\\ f = \\sum_{d \\in \\mathrm{supp}(f)} f_{d} \\cdot \\prod_{i \\in \\mathrm{supp}(d)} X_i^{d(i)}$$$

Lean4

theorem eval_eq (X : σ → R) (f : MvPolynomial σ R) :
    eval X f = ∑ d ∈ f.support, f.coeff d * ∏ i ∈ d.support, X i ^ d i :=
  rfl

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