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.

Instances For
    theorem RatFunc.laurentAux_ofFractionRing_mk {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : { x // x nonZeroDivisors (Polynomial R) }) :
    ↑(RatFunc.laurentAux r) { toFractionRing := Localization.mk p q } = { toFractionRing := Localization.mk (↑(Polynomial.taylor r) p) { val := ↑(Polynomial.taylor r) q, property := (_ : ↑(Polynomial.taylor r) q nonZeroDivisors (Polynomial R)) } }
    theorem RatFunc.laurentAux_div {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : Polynomial R) :
    ↑(RatFunc.laurentAux r) (↑(algebraMap (Polynomial R) (RatFunc R)) p / ↑(algebraMap (Polynomial R) (RatFunc R)) q) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p) / ↑(algebraMap ((fun x => Polynomial R) q) (RatFunc R)) (↑(Polynomial.taylor r) q)
    @[simp]
    theorem RatFunc.laurentAux_algebraMap {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) :
    ↑(RatFunc.laurentAux r) (↑(algebraMap (Polynomial R) (RatFunc R)) p) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p)
    def RatFunc.laurent {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) :

    The Laurent expansion of rational functions about a value.

    Instances For
      theorem RatFunc.laurent_div {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) (q : Polynomial R) :
      ↑(RatFunc.laurent r) (↑(algebraMap (Polynomial R) (RatFunc R)) p / ↑(algebraMap (Polynomial R) (RatFunc R)) q) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p) / ↑(algebraMap ((fun x => Polynomial R) q) (RatFunc R)) (↑(Polynomial.taylor r) q)
      @[simp]
      theorem RatFunc.laurent_algebraMap {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (p : Polynomial R) :
      ↑(RatFunc.laurent r) (↑(algebraMap (Polynomial R) (RatFunc R)) p) = ↑(algebraMap ((fun x => Polynomial R) p) (RatFunc R)) (↑(Polynomial.taylor r) p)
      @[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) :
      ↑(RatFunc.laurent 0) f = f
      theorem RatFunc.laurent_laurent {R : Type u} [CommRing R] [hdomain : IsDomain R] (r : R) (s : R) (f : RatFunc R) :
      ↑(RatFunc.laurent r) (↑(RatFunc.laurent s) f) = ↑(RatFunc.laurent (r + s)) f