evalEval_mk — Mathlib

English

If h: p.evalEval x y = 0, then evalEval h (mk p g) = g.evalEval x y; i.e., evaluation factors through AdjoinRoot when p vanishes at (x,y).

Русский

Если h: p.evalEval x y = 0, то evalEval h (mk p g) = g.evalEval x y; то есть вычисление факторизуется через AdjoinRoot при равенстве нулю p(x,y).

LaTeX

$$$\\text{evalEval} \\; h \\; (\\text{mk } p \\; g) = g \\text{evalEval } x y.$$$

Lean4

theorem evalEval_mk (g : R[X][Y]) : evalEval h (mk p g) = g.evalEval x y := by rw [evalEval, lift_mk, eval₂_evalRingHom]

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