invOfUnit — Mathlib

English

invOfUnit φ u is defined as inv.aux (↑u⁻¹) φ, i.e., the inverse series with constant coefficient equal to the inverse of u.

Русский

invOfUnit φ u задаётся как inv.aux (↑u⁻¹) φ, то есть обратная серия с константным коэффициентом равным обратному элементу u.

LaTeX

$$$ invOfUnit(φ, u) = inv.aux (↑u^{-1}) φ $$$

Lean4

/-- A multivariate formal power series is invertible if the constant coefficient is invertible. -/
def invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) : MvPowerSeries σ R :=
  inv.aux (↑u⁻¹) φ

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