eval_sub

Mathlib.Algebra.MvPolynomial.CommRing

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

English

For any p, q and linear evaluation map eval f, we have eval f (p − q) = eval f p − eval f q.

Русский

Для любых p, q и линейного отображения eval f выполняется eval f (p − q) = eval f p − eval f q.

LaTeX

$$$\\mathrm{eval}\, f\\, (p - q) = \\mathrm{eval}\, f\\, p - \\mathrm{eval}\, f\\, q$$$

Lean4

theorem eval_sub (f : σ → R) : eval f (p - q) = eval f p - eval f q :=
  eval₂_sub _ _ _

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

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

Разделы

Аффилиация

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