eval_neg

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

For any p ∈ R[X] and any x ∈ R, evaluating the negation of p equals the negation of the evaluation of p: (−p).eval x = − p.eval x.

Русский

Для любого p ∈ R[X] и любого x ∈ R выполняется (−p).eval x = − p.eval x.

LaTeX

$$$(-p).eval\\ x = -\\,p.eval\\ x$$$

Lean4

@[simp]
theorem eval_neg (p : R[X]) (x : R) : (-p).eval x = -p.eval x :=
  eval₂_neg _

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

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

Разделы

Аффилиация

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