eq_inv_iff_mul_eq_one — Mathlib

English

Let φ, ψ be power series in k⟨⟨X⟩⟧ with constantCoeff ψ ≠ 0. Then φ equals ψ^{-1} if and only if φ ψ equals 1.

Русский

Пусть φ, ψ — степенные ряды в k⟨⟨X⟧⟩ с c_0(ψ) ≠ 0. Тогда φ = ψ^{-1} тогда и только тогда, когда φ ψ = 1.

LaTeX

$$$ c_0(\psi) \neq 0 \Rightarrow (\psi^{-1} = \phi \iff \phi \psi = 1). $$$

Lean4

theorem eq_inv_iff_mul_eq_one {φ ψ : k⟦X⟧} (h : constantCoeff ψ ≠ 0) : φ = ψ⁻¹ ↔ φ * ψ = 1 :=
  MvPowerSeries.eq_inv_iff_mul_eq_one h

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