mathlib documentation


Laurent Series #

Main Definitions #

def laurent_series (R : Type u_1) [has_zero R] :
Type u_1

A laurent_series is implemented as a hahn_series with value group .

theorem laurent_series.coeff_coe_power_series {R : Type u_1} [semiring R] (x : power_series R) (n : ) :

This is a power series that can be multiplied by an integer power of X to give our Laurent series. If the Laurent series is nonzero, power_series_part has a nonzero constant term.


The localization map from power series to Laurent series.