constantCoeff — Mathlib

English

There is a natural ring homomorphism constantCoeff: R[[X]] → R extracting the constant term.

Русский

Существуют естественный гомоморфизм постоянного коэффициента: R[[X]] → R, выделяющий постоянный член.

LaTeX

$$$$ \operatorname{constantCoeff}: R[[X]] \to R \text{ is a ring homomorphism} $$$$

Lean4

/-- The constant coefficient of a formal power series. -/
def constantCoeff : R⟦X⟧ →+* R :=
  MvPowerSeries.constantCoeff

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