isUnit_constantCoeff — Mathlib

English

If φ is a unit (invertible) in the multivariate formal power series ring, then its constant coefficient is a unit in R.

Русский

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

LaTeX

$$$\\text{IsUnit}(\\phi) \\;\\Rightarrow\\; \\text{IsUnit}(\\operatorname{constantCoeff}(\\phi))$$$

Lean4

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

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