evalEval_neg

Mathlib.Algebra.Polynomial.Bivariate

URI: https://scilib.ai/kg/mathlib#Polynomial.evalEval_neg

English

Evaluation preserves negation: evaluate -p at (x,y) equals the negation of evaluating p at (x,y).

Русский

Оценка сохраняет противоположное: evaluate -p в (x,y) равно противоположному значению p в (x,y).

LaTeX

$$$ (-p).evalEval\\ x\\ y = - p.evalEval\\ x\\ y $$$

Lean4

@[simp]
theorem evalEval_neg (x y : R) (p : R[X][Y]) : (-p).evalEval x y = -p.evalEval x y := by simp only [evalEval, eval_neg]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru