invOfUnit — Mathlib

English

There is a construction invOfUnit φ u giving the inverse of a power series φ when its constant coefficient is a unit u.

Русский

Существует конструирование invOfUnit φ u, дающее обратную степеньному ряду φ при условии, что константный коэффициент φ — это юнит u.

LaTeX

$$$ invOfUnit(\varphi, u) = \text{(MvPowerSeries).invOfUnit}(\varphi, u) $$$

Lean4

/-- A formal power series is invertible if the constant coefficient is invertible. -/
def invOfUnit (φ : R⟦X⟧) (u : Rˣ) : R⟦X⟧ :=
  MvPowerSeries.invOfUnit φ u

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