isUnit_iff_constantCoeff — Mathlib

English

A power series φ is a unit iff its constant coefficient is a unit.

Русский

Степенной ряд φ является обратимым iff его константный коэффициент является единицей (юнитом).

LaTeX

$$$ \text{IsUnit}(φ) \iff \text{IsUnit}(\text{constantCoeff}(φ)) $$$

Lean4

theorem isUnit_iff_constantCoeff {φ : R⟦X⟧} : IsUnit φ ↔ IsUnit (constantCoeff φ) :=
  MvPowerSeries.isUnit_iff_constantCoeff

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