eval₂_eq — Mathlib

English

Explicit formula for f.eval₂ g X in terms of the support of p and the coeffs.

Русский

Явная формула для f.eval₂ g X через опору p и коэффициенты.

LaTeX

$$$f\eval_2\, g\, X\; p = \sum_{d \in \mathrm{support}(p)} g\bigl(p_{d}\bigr) \cdot \prod_{i \in \mathrm{support}(d)} X_i^{d(i)}$$$

Lean4

theorem eval₂_eq (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
    f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i ∈ d.support, X i ^ d i :=
  rfl

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