mathlib documentation

field_theory.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 alg_hom easier, which works on comm_ring which are not necessarily domains.

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
@[simp]
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
@[simp]
theorem ratfunc.laurent_algebra_map {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p : polynomial R) :
@[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) :
theorem ratfunc.laurent_laurent {R : Type u} [comm_ring R] [hdomain : is_domain R] (r s : R) (f : ratfunc R) :
theorem ratfunc.laurent_injective {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :