C_add

Mathlib.Algebra.MvPolynomial.Basic

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

English

The constant polynomial distributes over addition: C(a + a') = C(a) + C(a').

Русский

Константный полином распределяется по сложению: C(a + a') = C(a) + C(a').

LaTeX

$$$ C\ (a + a') = C\ a + C\ a' $$$

Lean4

@[simp]
theorem C_add : (C (a + a') : MvPolynomial σ R) = C a + C a' :=
  Finsupp.single_add _ _ _

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

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

Разделы

Аффилиация

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