Laurent Series

Main Definitions

• Defines LaurentSeries as an abbreviation for HahnSeries ℤ.
• Provides a coercion PowerSeries R into LaurentSeries R given by HahnSeries.ofPowerSeries.
• Defines LaurentSeries.powerSeriesPart
• Defines the localization map LaurentSeries.of_powerSeries_localization which evaluates to HahnSeries.ofPowerSeries.

@[inline, reducible]

abbrev LaurentSeries (R : Type u_1) [Zero R] : Type u_1

A LaurentSeries is implemented as a HahnSeries with value group ℤ.

Equations

• LaurentSeries R = HahnSeries ℤ R

instance LaurentSeries.instCoePowerSeriesLaurentSeriesToZeroToMonoidWithZero {R : Type u} [Semiring R] : Coe (PowerSeries R) (LaurentSeries R)

Equations

• LaurentSeries.instCoePowerSeriesLaurentSeriesToZeroToMonoidWithZero = { coe := ↑(HahnSeries.ofPowerSeries ℤ R) }

@[simp]

theorem LaurentSeries.coeff_coe_powerSeries {R : Type u} [Semiring R] (x : PowerSeries R) (n : ℕ) : HahnSeries.coeff (↑(HahnSeries.ofPowerSeries ℤ R) x) ↑n = ↑(PowerSeries.coeff R n) x

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

• LaurentSeries.powerSeriesPart x = PowerSeries.mk fun n => HahnSeries.coeff x (HahnSeries.order x + ↑n)

@[simp]

theorem LaurentSeries.powerSeriesPart_coeff {R : Type u} [Semiring R] (x : LaurentSeries R) (n : ℕ) : ↑(PowerSeries.coeff R n) (LaurentSeries.powerSeriesPart x) = HahnSeries.coeff x (HahnSeries.order x + ↑n)

@[simp]

theorem LaurentSeries.powerSeriesPart_zero {R : Type u} [Semiring R] : LaurentSeries.powerSeriesPart 0 = 0

@[simp]

theorem LaurentSeries.powerSeriesPart_eq_zero {R : Type u} [Semiring R] (x : LaurentSeries R) : LaurentSeries.powerSeriesPart x = 0 ↔ x = 0

@[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

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

instance LaurentSeries.instAlgebraPowerSeriesLaurentSeriesToZeroToCommMonoidWithZeroInstCommSemiringPowerSeriesInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingToSemiring {R : Type u} [CommSemiring R] : Algebra (PowerSeries R) (LaurentSeries R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LaurentSeries.coe_algebraMap {R : Type u} [CommSemiring R] : ↑(algebraMap (PowerSeries R) (LaurentSeries R)) = ↑(HahnSeries.ofPowerSeries ℤ R)

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

• @LaurentSeries.of_powerSeries_localization = @LaurentSeries.of_powerSeries_localization.proof_1

def LaurentSeries.instMonoidWithZeroHahnSeriesIntToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield {K : Type u} [Field K] : MonoidWithZero (HahnSeries ℤ K)

Equations

• LaurentSeries.instMonoidWithZeroHahnSeriesIntToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRingToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield = inferInstance

instance LaurentSeries.instIsFractionRingPowerSeriesInstCommRingPowerSeriesToCommRingToEuclideanDomainLaurentSeriesToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldInstCommRingHahnSeriesToPartialOrderToZeroToCommMonoidWithZeroToCommSemiringIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingInstAlgebraPowerSeriesLaurentSeriesToZeroToCommMonoidWithZeroInstCommSemiringPowerSeriesInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingToSemiringToCommSemiring {K : Type u} [Field K] : IsFractionRing (PowerSeries K) (LaurentSeries K)

Equations

• One or more equations did not get rendered due to their size.

theorem PowerSeries.coe_zero {R : Type u} [Semiring R] : ↑(HahnSeries.ofPowerSeries ℤ R) 0 = 0

theorem PowerSeries.coe_one {R : Type u} [Semiring R] : ↑(HahnSeries.ofPowerSeries ℤ R) 1 = 1

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

@[simp]

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'

@[simp]

theorem PowerSeries.coe_neg {R' : Type u_1} [Ring R'] (f' : PowerSeries R') : ↑(HahnSeries.ofPowerSeries ℤ R') (-f') = -↑(HahnSeries.ofPowerSeries ℤ R') f'

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

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

@[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

@[simp]

theorem PowerSeries.coe_pow {R : Type u} [Semiring R] (f : PowerSeries R) (n : ℕ) : ↑(HahnSeries.ofPowerSeries ℤ R) (f ^ n) = ↑(HahnSeries.ofPowerSeries ℤ R) f ^ n