coeff_zero_one

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

The coefficient at the zero index of the unit series is 1.

Русский

Коэффициент при нулевом индексе для единичного ряда равен 1.

LaTeX

$$$\\operatorname{coeff}(0 : σ \\to_0 \\mathbb{N}) (1) = 1$$$

Lean4

theorem coeff_zero_one : coeff (R := R) (0 : σ →₀ ℕ) 1 = 1 :=
  coeff_monomial_same 0 1

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

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

Разделы

Аффилиация

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