Laurent expansions of rational functions #

Main declarations #

• RatFunc.laurent: the Laurent expansion of the rational function f at r, as an AlgHom.
• RatFunc.laurent_injective: the Laurent expansion at r is unique

Implementation details #

Implemented as the quotient of two Taylor expansions, over domains. An auxiliary definition is provided first to make the construction of the AlgHom easier, which works on CommRing which are not necessarily domains.

theorem RatFunc.taylor_mem_nonZeroDivisors {R : Type u} [] (r : R) (p : ) (hp : ) :
p
def RatFunc.laurentAux {R : Type u} [] [hdomain : ] (r : R) :

The Laurent expansion of rational functions about a value. Auxiliary definition, usage when over integral domains should prefer RatFunc.laurent.

Equations
• = RatFunc.mapRingHom { toFun := , map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem RatFunc.laurentAux_ofFractionRing_mk {R : Type u} [] [hdomain : ] (r : R) (p : ) (q : ()) :
{ toFractionRing := } = { toFractionRing := Localization.mk ( p) q, }
theorem RatFunc.laurentAux_div {R : Type u} [] [hdomain : ] (r : R) (p : ) (q : ) :
((algebraMap () ()) p / (algebraMap () ()) q) = (algebraMap () ()) ( p) / (algebraMap () ()) ( q)
@[simp]
theorem RatFunc.laurentAux_algebraMap {R : Type u} [] [hdomain : ] (r : R) (p : ) :
((algebraMap () ()) p) = (algebraMap () ()) ( p)
def RatFunc.laurent {R : Type u} [] [hdomain : ] (r : R) :

The Laurent expansion of rational functions about a value.

Equations
Instances For
theorem RatFunc.laurent_div {R : Type u} [] [hdomain : ] (r : R) (p : ) (q : ) :
() ((algebraMap () ()) p / (algebraMap () ()) q) = (algebraMap () ()) ( p) / (algebraMap () ()) ( q)
@[simp]
theorem RatFunc.laurent_algebraMap {R : Type u} [] [hdomain : ] (r : R) (p : ) :
() ((algebraMap () ()) p) = (algebraMap () ()) ( p)
@[simp]
theorem RatFunc.laurent_X {R : Type u} [] [hdomain : ] (r : R) :
() RatFunc.X = RatFunc.X + RatFunc.C r
@[simp]
theorem RatFunc.laurent_C {R : Type u} [] [hdomain : ] (r : R) (x : R) :
() (RatFunc.C x) = RatFunc.C x
@[simp]
theorem RatFunc.laurent_at_zero {R : Type u} [] [hdomain : ] (f : ) :
() f = f
theorem RatFunc.laurent_laurent {R : Type u} [] [hdomain : ] (r : R) (s : R) (f : ) :
() (() f) = (RatFunc.laurent (r + s)) f
theorem RatFunc.laurent_injective {R : Type u} [] [hdomain : ] (r : R) :