mathlib3documentation

field_theory.laurent

Laurent expansions of rational functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

• ratfunc.laurent: the Laurent expansion of the rational function f at r, as an alg_hom.
• 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 alg_hom easier, which works on comm_ring which are not necessarily domains.

theorem ratfunc.taylor_mem_non_zero_divisors {R : Type u} [comm_ring R] (r : R) (p : polynomial R) (hp : p ) :
noncomputable def ratfunc.laurent_aux {R : Type u} [comm_ring R] (r : R) :

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

Equations
theorem ratfunc.laurent_aux_of_fraction_ring_mk {R : Type u} [comm_ring R] (r : R) (p : polynomial R) (q : ) :
theorem ratfunc.laurent_aux_div {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p q : polynomial R) :
( (ratfunc R)) p / (ratfunc R)) q) = (ratfunc R)) ( p) / (ratfunc R)) ( q)
@[simp]
theorem ratfunc.laurent_aux_algebra_map {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p : polynomial R) :
( (ratfunc R)) p) = (ratfunc R)) ( p)
noncomputable def ratfunc.laurent {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :

The Laurent expansion of rational functions about a value.

Equations
theorem ratfunc.laurent_div {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p q : polynomial R) :
( (ratfunc R)) p / (ratfunc R)) q) = (ratfunc R)) ( p) / (ratfunc R)) ( q)
@[simp]
theorem ratfunc.laurent_algebra_map {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p : polynomial R) :
( (ratfunc R)) p) = (ratfunc R)) ( p)
@[simp]
theorem ratfunc.laurent_X {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :
@[simp]
theorem ratfunc.laurent_C {R : Type u} [comm_ring R] [hdomain : is_domain R] (r x : R) :
@[simp]
theorem ratfunc.laurent_at_zero {R : Type u} [comm_ring R] [hdomain : is_domain R] (f : ratfunc R) :
f = f
theorem ratfunc.laurent_laurent {R : Type u} [comm_ring R] [hdomain : is_domain R] (r s : R) (f : ratfunc R) :
( f) = (ratfunc.laurent (r + s)) f
theorem ratfunc.laurent_injective {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :