coeff_zero_eq_constantCoeff_apply

Mathlib.RingTheory.MvPowerSeries.Basic

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

English

For any a ∈ R, constantCoeff (C a) = a.

Русский

Для любого a ∈ R, постоянный коэффициент C a равен a.

LaTeX

$$$\operatorname{constantCoeff}(C a) = a$$$

Lean4

theorem coeff_zero_eq_constantCoeff_apply (φ : MvPowerSeries σ R) : coeff (0 : σ →₀ ℕ) φ = constantCoeff φ :=
  rfl

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

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

Разделы

Аффилиация

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