Documentation

Mathlib.RingTheory.HahnSeries.HEval

A summable family given by a power series #

Main Definitions #

TODO #

@[reducible, inline]

A summable family given by scalar multiples of powers of a positive order Hahn series.

The scalar multiples are given by the coefficients of a power series.

Equations
Instances For
    @[simp]