mul_inv_rev — Mathlib

English

In the ring of formal power series k⟦X⟧, the inverse of a product equals the reversed product of inverses: (φ ψ)^{-1} = ψ^{-1} φ^{-1}.

Русский

В кольце формальных степенных рядов k⟦X⟧ обратный к произведению равен произведению обратных в обратном порядке: (φ ψ)^{-1} = ψ^{-1} φ^{-1}.

LaTeX

$$$ (\phi \cdot \psi)^{-1} = \psi^{-1} \cdot \phi^{-1}. $$$

Lean4

protected theorem mul_inv_rev (φ ψ : k⟦X⟧) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
  MvPowerSeries.mul_inv_rev _ _

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