mul_inv_cancel — Mathlib

English

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

Русский

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

LaTeX

$$$$ \operatorname{constCoeff}(\phi) \neq 0 \implies \phi \cdot \phi^{-1} = 1 \quad\text{and}\quad \phi^{-1} \cdot \phi = 1. $$$$

Lean4

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

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