isUnit_iff_constantCoeff — Mathlib

English

For any φ, φ is a unit iff its constantCoeff is a unit.

Русский

Для любого φ: φ является единицей тогда и только тогда, когда его константный коэффициент является единицей.

LaTeX

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

Lean4

theorem isUnit_iff_constantCoeff {φ : MvPowerSeries σ R} : IsUnit φ ↔ IsUnit (constantCoeff φ) :=
  by
  constructor
  · exact IsUnit.map _
  · intro ⟨u, hu⟩
    exact ⟨⟨_, φ.invOfUnit u, mul_invOfUnit φ u hu.symm, invOfUnit_mul φ u hu.symm⟩, rfl⟩

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