degrees_C

Mathlib.Algebra.MvPolynomial.Degrees

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

English

For any a in R, deg(C a) = 0.

Русский

Для любого a в R, deg(C a) = 0.

LaTeX

$$$\deg(C a) = 0\quad(a \in R)$$$

Lean4

theorem degrees_C (a : R) : degrees (C a : MvPolynomial σ R) = 0 :=
  Multiset.le_zero.1 <| degrees_monomial _ _

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

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

Разделы

Аффилиация

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