coeff_zero_eq_constantCoeff

Mathlib.RingTheory.PowerSeries.Basic

URI: https://scilib.ai/kg/mathlib#PowerSeries.coeff_zero_eq_constantCoeff

English

For any φ, the 0-th coefficient equals the constantCoeff of φ.

Русский

Для любого φ нулевой коэффициент равен constantCoeff(φ).

LaTeX

$$$$ \operatorname{coeff}_0(\phi) = \operatorname{constantCoeff}(\phi) $$$$

Lean4

@[simp]
theorem coeff_zero_eq_constantCoeff : ⇑(coeff (R := R) 0) = constantCoeff :=
  by
  rw [coeff, Finsupp.single_zero]
  rfl

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

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

Разделы

Аффилиация

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