inv — Mathlib

English

The inverse of a multivariate power series φ ∈ MvPowerSeries σ k over a field k is defined by inv φ = inv.aux (constantCoeff φ)⁻¹ φ.

Русский

Обратная к φ ∈ MvPowerSeries σ k по полю k задаётся как inv φ = inv.aux (constantCoeff φ)⁻¹ φ.

LaTeX

$$$ \mathrm{inv}(\varphi) = \mathrm{inv.aux}(\operatorname{constantCoeff}(\varphi))^{-1} \; \varphi $$$

Lean4

/-- The inverse `1/f` of a multivariable power series `f` over a field -/
protected def inv (φ : MvPowerSeries σ k) : MvPowerSeries σ k :=
  inv.aux (constantCoeff φ)⁻¹ φ

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