instDivInvMonoid — Mathlib

English

For x with 0 < x.orderTop, for each g the set { a | ((x^a).coeff g) ≠ 0 } is finite.

Русский

Для x с 0 < x.orderTop для каждого g множество { a | ((x^a).coeff g) ≠ 0 } конечно.

LaTeX

$$$\{a \in \mathbb{N} \mid (x^a).coeff(g) \neq 0\} \text{ is finite}$$$

Lean4

@[simps -isSimp inv]
instance : DivInvMonoid (HahnSeries Γ R) where
  inv
    x :=
    single (-x.order) (x.leadingCoeff)⁻¹ * (SummableFamily.powers <| 1 - single (-x.order) (x.leadingCoeff)⁻¹ * x).hsum

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