neg_def

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.neg_def

English

The negated polynomial law is obtained by scaling by -1 on each coefficient.

Русский

Отрицательный полиномальный закон получается умножением на -1 на каждом коэффициенте.

LaTeX

$$ $(-f)^{\mathrm{toFun}'}_S = (-1)\cdot f^{\mathrm{toFun}'}_S$.$$

Lean4

@[simp]
theorem neg_def (S : Type u) [CommSemiring S] [Algebra R S] : (-f).toFun' S = (-1 : R) • f.toFun' S :=
  rfl

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

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

Разделы

Аффилиация

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