Documentation

Mathlib.RingTheory.LaurentSeries

Laurent Series #

Main Definitions #

source
@[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
    source
    instance LaurentSeries.instCoePowerSeriesLaurentSeriesToZeroToMonoidWithZero {R : Type u} [Semiring R] :
    Coe (PowerSeries R) (LaurentSeries R)
    Equations
    source
    @[simp]
    theorem LaurentSeries.coeff_coe_powerSeries {R : Type u} [Semiring R] (x : PowerSeries R) (n : ℕ) :
    ((HahnSeries.ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff R n) x
    source
    def LaurentSeries.powerSeriesPart {R : Type u} [Semiring R] (x : LaurentSeries R) :
    PowerSeries R

    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
      source
      @[simp]
      theorem LaurentSeries.powerSeriesPart_coeff {R : Type u} [Semiring R] (x : LaurentSeries R) (n : ℕ) :
      (PowerSeries.coeff R n) (LaurentSeries.powerSeriesPart x) = x.coeff (HahnSeries.order x + ↑n)
      source
      @[simp]
      theorem LaurentSeries.powerSeriesPart_zero {R : Type u} [Semiring R] :
      LaurentSeries.powerSeriesPart 0 = 0
      source
      @[simp]
      theorem LaurentSeries.powerSeriesPart_eq_zero {R : Type u} [Semiring R] (x : LaurentSeries R) :
      LaurentSeries.powerSeriesPart x = 0 ↔ x = 0
      source
      @[simp]
      theorem LaurentSeries.single_order_mul_powerSeriesPart {R : Type u} [Semiring R] (x : LaurentSeries R) :
      (HahnSeries.single (HahnSeries.order x)) 1 * (HahnSeries.ofPowerSeries ℤ R) (LaurentSeries.powerSeriesPart x) = x
      source
      theorem LaurentSeries.ofPowerSeries_powerSeriesPart {R : Type u} [Semiring R] (x : LaurentSeries R) :
      (HahnSeries.ofPowerSeries ℤ R) (LaurentSeries.powerSeriesPart x) = (HahnSeries.single (-HahnSeries.order x)) 1 * x
      source
      instance LaurentSeries.instAlgebraPowerSeriesLaurentSeriesToZeroToCommMonoidWithZeroInstCommSemiringPowerSeriesInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingToSemiring {R : Type u} [CommSemiring R] :
      Algebra (PowerSeries R) (LaurentSeries R)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem LaurentSeries.coe_algebraMap {R : Type u} [CommSemiring R] :
      ⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = ⇑(HahnSeries.ofPowerSeries ℤ R)
      source
      instance LaurentSeries.of_powerSeries_localization {R : Type u} [CommRing R] :
      IsLocalization (Submonoid.powers PowerSeries.X) (LaurentSeries R)

      The localization map from power series to Laurent series.

      Equations
      source
      def LaurentSeries.instMonoidWithZeroHahnSeriesIntToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield {K : Type u} [Field K] :
      MonoidWithZero (HahnSeries ℤ K)
      Equations
      • LaurentSeries.instMonoidWithZeroHahnSeriesIntToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield = inferInstance
      Instances For
        source
        instance LaurentSeries.instIsFractionRingPowerSeriesInstCommRingPowerSeriesToCommRingToEuclideanDomainLaurentSeriesToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldInstCommRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZeroToCommSemiringIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingInstAlgebraPowerSeriesLaurentSeriesToZeroToCommMonoidWithZeroInstCommSemiringPowerSeriesInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingToSemiringToCommSemiring {K : Type u} [Field K] :
        IsFractionRing (PowerSeries K) (LaurentSeries K)
        Equations
        source
        theorem PowerSeries.coe_zero {R : Type u} [Semiring R] :
        (HahnSeries.ofPowerSeries ℤ R) 0 = 0
        source
        theorem PowerSeries.coe_one {R : Type u} [Semiring R] :
        (HahnSeries.ofPowerSeries ℤ R) 1 = 1
        source
        theorem PowerSeries.coe_add {R : Type u} [Semiring R] (f : PowerSeries R) (g : PowerSeries R) :
        (HahnSeries.ofPowerSeries ℤ R) (f + g) = (HahnSeries.ofPowerSeries ℤ R) f + (HahnSeries.ofPowerSeries ℤ R) g
        source
        theorem PowerSeries.coe_sub {R' : Type u_1} [Ring R'] (f' : PowerSeries R') (g' : PowerSeries R') :
        (HahnSeries.ofPowerSeries ℤ R') (f' - g') = (HahnSeries.ofPowerSeries ℤ R') f' - (HahnSeries.ofPowerSeries ℤ R') g'
        source
        theorem PowerSeries.coe_neg {R' : Type u_1} [Ring R'] (f' : PowerSeries R') :
        (HahnSeries.ofPowerSeries ℤ R') (-f') = -(HahnSeries.ofPowerSeries ℤ R') f'
        source
        theorem PowerSeries.coe_mul {R : Type u} [Semiring R] (f : PowerSeries R) (g : PowerSeries R) :
        (HahnSeries.ofPowerSeries ℤ R) (f * g) = (HahnSeries.ofPowerSeries ℤ R) f * (HahnSeries.ofPowerSeries ℤ R) g
        source
        theorem PowerSeries.coeff_coe {R : Type u} [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
        source
        theorem PowerSeries.coe_C {R : Type u} [Semiring R] (r : R) :
        (HahnSeries.ofPowerSeries ℤ R) ((PowerSeries.C R) r) = HahnSeries.C r
        source
        theorem PowerSeries.coe_X {R : Type u} [Semiring R] :
        (HahnSeries.ofPowerSeries ℤ R) PowerSeries.X = (HahnSeries.single 1) 1
        source
        @[simp]
        theorem PowerSeries.coe_smul {R : Type u} [Semiring R] {S : Type u_2} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) :
        (HahnSeries.ofPowerSeries ℤ S) (r • x) = r • (HahnSeries.ofPowerSeries ℤ S) x
        source
        @[simp]
        theorem PowerSeries.coe_pow {R : Type u} [Semiring R] (f : PowerSeries R) (n : ℕ) :
        (HahnSeries.ofPowerSeries ℤ R) (f ^ n) = (HahnSeries.ofPowerSeries ℤ R) f ^ n