mathlib3 documentation

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 #

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
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]
@[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) :