isUnit_constantCoeff — Mathlib

English

If a power series φ is a unit, then its constant coefficient is a unit of the base ring.

Русский

Если ряд φ является единицей, то его постоянный коэффициент тоже единица в базовом кольце.

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R],\\\\; \\text{IsUnit }\\varphi \\Rightarrow \\text{IsUnit}(\\operatorname{constantCoeff}(\\varphi))$$$

Lean4

/-- If a formal power series is invertible, then so is its constant coefficient. -/
theorem isUnit_constantCoeff (φ : R⟦X⟧) (h : IsUnit φ) : IsUnit (constantCoeff φ) :=
  MvPowerSeries.isUnit_constantCoeff φ h

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