inv_mul_cancel — Mathlib

English

If φ ∈ k⟦X⟧ has nonzero constant term, then φ⁻¹ · φ = 1 and φ · φ⁻¹ = 1.

Русский

Если φ ∈ k⟦X⟧ имеет ненулевой коэффициент при 0-ой степени, то φ⁻¹ · φ = 1 и φ · φ⁻¹ = 1.

LaTeX

$$$$ \phi \neq 0 \implies \phi^{-1} \cdot \phi = 1. $$$$

Lean4

@[simp]
protected theorem inv_mul_cancel (φ : k⟦X⟧) (h : constantCoeff φ ≠ 0) : φ⁻¹ * φ = 1 :=
  MvPowerSeries.inv_mul_cancel φ h

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