coeff_zero_one

Mathlib.Algebra.MvPolynomial.Basic

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

English

Coefficient at 0 of a constant C equals C: coeff 0 (C a) = a.

Русский

Коэффициент 0 константы равен её константному коэффициенту.

LaTeX

$$$\mathrm{coeff}\;0\ (C\ a) = a$$$

Lean4

@[simp]
theorem coeff_zero_one : coeff 0 (1 : MvPolynomial σ R) = 1 :=
  coeff_zero_C 1

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

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

Разделы

Аффилиация

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