coeff_zero_eq_constantCoeff

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

For any φ, coeff(0) φ = constantCoeff φ.

Русский

Для любого φ выполнено: coeff(0) φ = constantCoeff φ.

LaTeX

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

Lean4

@[simp]
theorem coeff_zero_eq_constantCoeff : ⇑(coeff (R := R) (0 : σ →₀ ℕ)) = constantCoeff :=
  rfl

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

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

Разделы

Аффилиация

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