Laurent Series #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main Definitions #
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
The localization map from power series to Laurent series.