Laurent Series #

Main Definitions #

@[inline, reducible]
abbrev LaurentSeries (R : Type u_1) [Zero R] :
Type u_1

A LaurentSeries is implemented as a HahnSeries with value group .

Instances For

    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, powerSeriesPart has a nonzero constant term.

    Instances For

      The localization map from power series to Laurent series.

      theorem PowerSeries.coe_sub {R' : Type u_1} [Ring R'] (f' : PowerSeries R') (g' : PowerSeries R') :
      theorem PowerSeries.coe_neg {R' : Type u_1} [Ring R'] (f' : PowerSeries R') :
      theorem PowerSeries.coeff_coe {R : Type u} [Semiring R] (f : PowerSeries R) (i : ) :
      HahnSeries.coeff (↑(HahnSeries.ofPowerSeries R) f) i = if i < 0 then 0 else ↑(PowerSeries.coeff R (Int.natAbs i)) f
      theorem PowerSeries.coe_C {R : Type u} [Semiring R] (r : R) :
      ↑(HahnSeries.ofPowerSeries R) (↑(PowerSeries.C R) r) = HahnSeries.C r
      theorem PowerSeries.coe_X {R : Type u} [Semiring R] :
      ↑(HahnSeries.ofPowerSeries R) PowerSeries.X = ↑(HahnSeries.single 1) 1
      theorem PowerSeries.coe_smul {R : Type u} [Semiring R] {S : Type u_2} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) :
      theorem PowerSeries.coe_pow {R : Type u} [Semiring R] (f : PowerSeries R) (n : ) :