eq_inv_iff_mul_eq_one — Mathlib

English

Let φ, ψ be multivariate power series with ψ having nonzero constant coefficient. Then φ equals ψ⁻¹ if and only if φ ψ equals the multiplicative identity 1.

Русский

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

LaTeX

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

Lean4

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

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