# Laurent Series #

## Main Definitions #

• Defines LaurentSeries as an abbreviation for HahnSeries ℤ.
• Defines hasseDeriv of a Laurent series with coefficients in a module over a ring.
• 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.
• Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying RatFunc.coeAlgHom.

## Main Results #

• Basic properties of Hasse derivatives
@[reducible, inline]
abbrev LaurentSeries (R : Type u) [Zero R] :

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

Equations
Instances For
@[simp]
theorem LaurentSeries.hasseDeriv_apply (R : Type u_2) {V : Type u_3} [] [] [Module R V] (k : ) (f : ) :
() f = HahnSeries.ofSuppBddBelow (fun (n : ) => Ring.choose (n + k) k f.coeff (n + k))
def LaurentSeries.hasseDeriv (R : Type u_2) {V : Type u_3} [] [] [Module R V] (k : ) :

The Hasse derivative of Laurent series, as a linear map.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem LaurentSeries.hasseDeriv_coeff {R : Type u_1} [] {V : Type u_2} [] [Module R V] (k : ) (f : ) (n : ) :
(() f).coeff n = Ring.choose (n + k) k f.coeff (n + k)
instance LaurentSeries.instCoePowerSeries {R : Type u_1} [] :
Coe () ()
Equations
• LaurentSeries.instCoePowerSeries = { coe := }
@[simp]
theorem LaurentSeries.coeff_coe_powerSeries {R : Type u_1} [] (x : ) (n : ) :
().coeff n = () x
def LaurentSeries.powerSeriesPart {R : Type u_1} [] (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
@[simp]
theorem LaurentSeries.powerSeriesPart_coeff {R : Type u_1} [] (x : ) (n : ) :
() x.powerSeriesPart = x.coeff ()
@[simp]
@[simp]
theorem LaurentSeries.powerSeriesPart_eq_zero {R : Type u_1} [] (x : ) :
x.powerSeriesPart = 0 x = 0
@[simp]
theorem LaurentSeries.single_order_mul_powerSeriesPart {R : Type u_1} [] (x : ) :
* x.powerSeriesPart = x
theorem LaurentSeries.ofPowerSeries_powerSeriesPart {R : Type u_1} [] (x : ) :
x.powerSeriesPart = * x
Equations
• LaurentSeries.instAlgebraPowerSeries = .toAlgebra
@[simp]
theorem LaurentSeries.coe_algebraMap {R : Type u_1} [] :
() =

The localization map from power series to Laurent series.

Equations
• =
Equations
• =
theorem PowerSeries.coe_zero {R : Type u_1} [] :
= 0
theorem PowerSeries.coe_one {R : Type u_1} [] :
= 1
theorem PowerSeries.coe_add {R : Type u_1} [] (f : ) (g : ) :
(f + g) = +
theorem PowerSeries.coe_sub {R' : Type u_2} [Ring R'] (f' : ) (g' : ) :
(f' - g') = f' - g'
theorem PowerSeries.coe_neg {R' : Type u_2} [Ring R'] (f' : ) :
(-f') = - f'
theorem PowerSeries.coe_mul {R : Type u_1} [] (f : ) (g : ) :
(f * g) = *
theorem PowerSeries.coeff_coe {R : Type u_1} [] (f : ) (i : ) :
().coeff i = if i < 0 then 0 else (PowerSeries.coeff R i.natAbs) f
theorem PowerSeries.coe_C {R : Type u_1} [] (r : R) :
(() r) = HahnSeries.C r
theorem PowerSeries.coe_X {R : Type u_1} [] :
PowerSeries.X = 1
@[simp]
theorem PowerSeries.coe_smul {R : Type u_1} [] {S : Type u_3} [] [Module R S] (r : R) (x : ) :
(r x) = r
theorem PowerSeries.coe_pow {R : Type u_1} [] (f : ) (n : ) :
(f ^ n) = ^ n
def RatFunc.coeAlgHom (F : Type u) [] :

The coercion RatFunc F → LaurentSeries F as bundled alg hom.

Equations
Instances For
def RatFunc.coeToLaurentSeries_fun {F : Type u} [] :

The coercion RatFunc F → LaurentSeries F as a function.

This is the implementation of coeToLaurentSeries.

Equations
• RatFunc.coeToLaurentSeries_fun =
Instances For
instance RatFunc.coeToLaurentSeries {F : Type u} [] :
Coe () ()
Equations
• RatFunc.coeToLaurentSeries = { coe := RatFunc.coeToLaurentSeries_fun }
theorem RatFunc.coe_def {F : Type u} [] (f : ) :
f = f
theorem RatFunc.coe_num_denom {F : Type u} [] (f : ) :
f = f.num / f.denom
theorem RatFunc.coe_injective {F : Type u} [] :
Function.Injective RatFunc.coeToLaurentSeries_fun
@[simp]
theorem RatFunc.coe_apply {F : Type u} [] (f : ) :
f = f
theorem RatFunc.coe_coe {F : Type u} [] (P : ) :
P = P
@[simp]
theorem RatFunc.coe_zero {F : Type u} [] :
0 = 0
theorem RatFunc.coe_ne_zero {F : Type u} [] {f : } (hf : f 0) :
f 0
@[simp]
theorem RatFunc.coe_one {F : Type u} [] :
1 = 1
@[simp]
theorem RatFunc.coe_add {F : Type u} [] (f : ) (g : ) :
(f + g) = f + g
@[simp]
theorem RatFunc.coe_sub {F : Type u} [] (f : ) (g : ) :
(f - g) = f - g
@[simp]
theorem RatFunc.coe_neg {F : Type u} [] (f : ) :
(-f) = -f
@[simp]
theorem RatFunc.coe_mul {F : Type u} [] (f : ) (g : ) :
(f * g) = f * g
@[simp]
theorem RatFunc.coe_pow {F : Type u} [] (f : ) (n : ) :
(f ^ n) = f ^ n
@[simp]
theorem RatFunc.coe_div {F : Type u} [] (f : ) (g : ) :
(f / g) = f / g
@[simp]
theorem RatFunc.coe_C {F : Type u} [] (r : F) :
(RatFunc.C r) = HahnSeries.C r
@[simp]
theorem RatFunc.coe_smul {F : Type u} [] (f : ) (r : F) :
(r f) = r f
@[simp]
theorem RatFunc.coe_X {F : Type u} [] :
RatFunc.X = 1
theorem RatFunc.single_one_eq_pow {R : Type u_2} [Ring R] (n : ) :
() 1 = 1 ^ n
theorem RatFunc.single_inv {F : Type u} [] (d : ) {α : F} (hα : α 0) :
() α⁻¹ = ( α)⁻¹
theorem RatFunc.single_zpow {F : Type u} [] (n : ) :
1 = 1 ^ n
instance RatFunc.instAlgebraLaurentSeries {F : Type u} [] :
Algebra () ()
Equations
• RatFunc.instAlgebraLaurentSeries = .toAlgebra
theorem RatFunc.algebraMap_apply_div {F : Type u} [] (p : ) (q : ) :
(algebraMap () ()) ((algebraMap () ()) p / (algebraMap () ()) q) = () p / () q
Equations
• =