eval_neg

Mathlib.Algebra.MvPolynomial.CommRing

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

English

The evaluation with a function f and g preserves negation: eval₂ f g (−p) = − eval₂ f g p.

Русский

Эвалюация сохраняет отрицание: eval₂ f g (−p) = − eval₂ f g p.

LaTeX

$$$\\mathrm{eval}_2 f g (-p) = -\\mathrm{eval}_2 f g p$$$

Lean4

theorem eval_neg (f : σ → R) : eval f (-p) = -eval f p :=
  eval₂_neg _ _ _

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

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

Разделы

Аффилиация

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