coeff_one

Mathlib.Algebra.MvPolynomial.Basic

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

English

The coefficient of 1 at m equals the standard C-coefficient: coeff m 1 = if 0 = m then 1 else 0.

Русский

Коэффициент при m в единице: coeff m 1 = если 0=m тогда 1 иначе 0.

LaTeX

$$$\mathrm{coeff}\;m\;1 = \mathrm{iff}\ 0=m\ \text{then } 1\ else\ 0$$$

Lean4

theorem coeff_one [DecidableEq σ] (m) : coeff m (1 : MvPolynomial σ R) = if 0 = m then 1 else 0 :=
  coeff_C m 1

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

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

Разделы

Аффилиация

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