C_sub

Mathlib.Algebra.MvPolynomial.CommRing

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

English

For all a, a' in R, the constant polynomial of a − a' equals the difference of the constant polynomials Ca and Ca'.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem C_sub : (C (a - a') : MvPolynomial σ R) = C a - C a' :=
  RingHom.map_sub _ _ _

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

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

Разделы

Аффилиация

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