constantCoeff — Mathlib

English

The map sending a series to its 0-th coefficient equals the constantCoeff map: coeff 0 = constantCoeff.

Русский

Пусть отображение φ ↦ coeff 0 φ совпадает с отображением φ ↦ constantCoeff φ.

LaTeX

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

Lean4

/-- The constant coefficient of a formal power series. -/
def constantCoeff : MvPowerSeries σ R →+* R :=
  { coeff (0 : σ →₀ ℕ) with
    toFun := coeff (0 : σ →₀ ℕ)
    map_one' := coeff_zero_one
    map_mul' := fun φ ψ => by classical simp [coeff_mul]
    map_zero' := LinearMap.map_zero _ }

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