inv_eq_iff_mul_eq_one — Mathlib

English

Let φ, ψ be multivariate power series with ψ constantCoeff nonzero. Then ψ⁻¹ = φ iff φ ψ = 1.

Русский

Пусть ψ — многовариантный формальный ряд с ненулевым константным коэффициентом. Тогда ψ⁻¹ = φ тогда и только тогда, когда φ ψ = 1.

LaTeX

$$$\forall \phi, \psi \in \mathrm{MvPowerSeries}(\sigma,k),\; \operatorname{constantCoeff}(\psi) \neq 0 \Rightarrow (\psi^{-1} = \phi \iff \phi \psi = 1)$$$

Lean4

protected theorem inv_eq_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff ψ ≠ 0) : ψ⁻¹ = φ ↔ φ * ψ = 1 := by
  rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h]

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