eval₂ — Mathlib

English

Evaluate a multivariate polynomial by fixing the value of each variable via a valuation, together with a ring hom for scalars.

Русский

Оценить многочлен со множеством переменных, фиксацией значений каждой переменной через оценку и кольцевого однозначного гомоморфа для скаляров.

LaTeX

$$$\mathrm{eval_2}(p) = \sum_{d \in \mathrm{support}(p)} f(a) \cdot \prod_{i \in \mathrm{support}(d)} g(i)^{d(i)}$$$

Lean4

/-- Evaluate a polynomial `p` given a valuation `g` of all the variables
  and a ring hom `f` from the scalar ring to the target -/
def eval₂ (p : MvPolynomial σ R) : S₁ :=
  p.sum fun s a => f a * s.prod fun n e => g n ^ e

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