invUnitsSub — Mathlib

English

The power-series invUnitsSub satisfies a simple relation with X, namely a specific linear combination with the constant term.

Русский

У invUnitsSub имеется простое отношение к X: определённая линейная комбинация с константным слагаемым.

LaTeX

$$$invUnitsSub(u) \cdot X = invUnitsSub(u) \cdot C(u) - 1$$$

Lean4

/-- The power series for `1 / (u - x)`. -/
def invUnitsSub (u : Rˣ) : PowerSeries R :=
  mk fun n => 1 /ₚ u ^ (n + 1)

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