invOfUnit_eq — Mathlib

English

Let φ ∈ k[[X]] have nonzero constant term. Then φ is a unit, and its multiplicative inverse is φ⁻¹; in particular φ · φ⁻¹ = φ⁻¹ · φ = 1.

Русский

Пусть φ ∈ k[[X]] имеет ненулевой коэффициент при X⁰. Тогда φ — единица, и её обратная последовательность равна φ⁻¹; то есть φ · φ⁻¹ = φ⁻¹ · φ = 1.

LaTeX

$$$$ \operatorname{constCoeff}(\phi) \neq 0 \implies \phi \cdot \phi^{-1} = 1 \;\land\; \phi^{-1} \cdot \phi = 1. $$$$

Lean4

@[simp]
theorem invOfUnit_eq (φ : k⟦X⟧) (h : constantCoeff φ ≠ 0) : invOfUnit φ (Units.mk0 _ h) = φ⁻¹ :=
  rfl

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