evalEval — Mathlib

English

Let R be a semiring and p ∈ R[X][Y]. The two-variable evaluation evalEval(x,y,p) equals p evaluated at (x,y).

Русский

Пусть R — полукольцо; p ∈ R[X][Y]. Вдвупеременная оценка evalEval(x,y,p) равна p, последовательной по (x,y).

LaTeX

$$$$\operatorname{evalEval}(x,y,p) = p(x,y).$$$$

Lean4

/-- `evalEval x y p` is the evaluation `p(x,y)` of a two-variable polynomial `p : R[X][Y]`. -/
abbrev evalEval (x y : R) (p : R[X][Y]) : R :=
  eval x (eval (C y) p)

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