smeval_neg

Mathlib.Algebra.Polynomial.Smeval

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

English

Smeval respects negation: smeval(-p) = -smeval(p).

Русский

Smeval сохраняет отрицание: smeval(-p) = -smeval(p).

LaTeX

$$$$ ( -p ).smeval x = - p.smeval x. $$$$

Lean4

@[simp]
theorem smeval_neg : (-p).smeval x = -p.smeval x := by
  rw [← add_eq_zero_iff_eq_neg, ← smeval_add, neg_add_cancel, smeval_zero]

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

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

Разделы

Аффилиация

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