Documentation

Mathlib.RingTheory.LaurentSeries

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 .

Equations
Instances For
    Equations
    @[simp]
    theorem LaurentSeries.coeff_coe_powerSeries {R : Type u_1} [Semiring R] (x : PowerSeries R) (n : ) :
    ((HahnSeries.ofPowerSeries R) x).coeff n = (PowerSeries.coeff R n) x

    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.

    Equations
    Instances For

      The localization map from power series to Laurent series.

      Equations
      • =
      Equations
      • LaurentSeries.instMonoidWithZeroHahnSeriesIntToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield = inferInstance
      Instances For
        theorem PowerSeries.coeff_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) (i : ) :
        ((HahnSeries.ofPowerSeries R) f).coeff i = if i < 0 then 0 else (PowerSeries.coeff R (Int.natAbs i)) f
        theorem PowerSeries.coe_C {R : Type u_1} [Semiring R] (r : R) :
        (HahnSeries.ofPowerSeries R) ((PowerSeries.C R) r) = HahnSeries.C r
        @[simp]
        theorem PowerSeries.coe_smul {R : Type u_1} [Semiring R] {S : Type u_3} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) :
        @[simp]