C_neg

Mathlib.Algebra.MvPolynomial.CommRing

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

English

For all a in R, the constant polynomial of −a equals the negation of the constant polynomial of a.

Русский

Для любого a в R константный многочлен −a равен отрицанию константного многочлена a.

LaTeX

$$$C(-a) = -C(a)$$$

Lean4

@[simp]
theorem C_neg : (C (-a) : MvPolynomial σ R) = -C a :=
  RingHom.map_neg _ _

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

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

Разделы

Аффилиация

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