evalEval_C — Mathlib

English

For any x,y ∈ R and p ∈ R[X], (C p).evalEval x y = p.eval x; i.e., evaluating a constant in two variables reduces to one-variable evaluation.

Русский

Для любых x,y ∈ R и p ∈ R[X] выполняется (C p).evalEval x y = p.eval x; то есть двупеременная оценка константы сводится к однопеременной оценке.

LaTeX

$$$$ (\mathrm{C} p).\mathrm{evalEval} x y = \mathrm{eval} \ x (\mathrm{eval} (\mathrm{C} y) p). $$$$

Lean4

theorem evalEval_C (x y : R) (p : R[X]) : (C p).evalEval x y = p.eval x := by rw [evalEval, eval_C]

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