Documentation

Mathlib.FieldTheory.Laurent

Laurent expansions of rational functions #

Main declarations #

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.

def RatFunc.laurentAux {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) :

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

Equations
Instances For
    theorem RatFunc.laurentAux_ofFractionRing_mk {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : (nonZeroDivisors (Polynomial R))) :
    (RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } = { toFractionRing := Localization.mk ((Polynomial.taylor r) p) (Polynomial.taylor r) q, }
    @[simp]
    theorem RatFunc.laurentAux_algebraMap {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) :
    def RatFunc.laurent {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) :

    The Laurent expansion of rational functions about a value.

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