# mathlib3documentation

ring_theory.laurent_series

# Laurent Series #

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

## Main Definitions #

• Defines laurent_series as an abbreviation for hahn_series ℤ.
• Provides a coercion power_series R into laurent_series R given by hahn_series.of_power_series.
• Defines laurent_series.power_series_part
• Defines the localization map laurent_series.of_power_series_localization which evaluates to hahn_series.of_power_series.
@[reducible]
def laurent_series (R : Type u_1) [has_zero R] :
Type u_1

A laurent_series is implemented as a hahn_series with value group ℤ.

@[protected, instance]
noncomputable def laurent_series.has_coe {R : Type u} [semiring R] :
Equations
@[simp]
theorem laurent_series.coeff_coe_power_series {R : Type u} [semiring R] (x : power_series R) (n : ) :
x.coeff n = n) x
noncomputable def laurent_series.power_series_part {R : Type u} [semiring R] (x : laurent_series R) :

This is a power series that can be multiplied by an integer power of X to give our Laurent series. If the Laurent series is nonzero, power_series_part has a nonzero constant term.

Equations
@[simp]
@[simp]
@[protected, instance]
noncomputable def laurent_series.algebra {R : Type u}  :
Equations
@[simp]
@[protected, instance]

The localization map from power series to Laurent series.

@[protected, instance]
@[simp, norm_cast]
theorem power_series.coe_zero {R : Type u} [semiring R] :
0 = 0
@[simp, norm_cast]
theorem power_series.coe_one {R : Type u} [semiring R] :
1 = 1
@[simp, norm_cast]
theorem power_series.coe_add {R : Type u} [semiring R] (f g : power_series R) :
(f + g) = f + g
@[simp, norm_cast]
theorem power_series.coe_sub {R' : Type u_1} [ring R'] (f' g' : power_series R') :
(f' - g') = f' - g'
@[simp, norm_cast]
theorem power_series.coe_neg {R' : Type u_1} [ring R'] (f' : power_series R') :
-f' = -f'
@[simp, norm_cast]
theorem power_series.coe_mul {R : Type u} [semiring R] (f g : power_series R) :
(f * g) = f * g
theorem power_series.coeff_coe {R : Type u} [semiring R] (f : power_series R) (i : ) :
f.coeff i = ite (i < 0) 0 ( f)
@[simp, norm_cast]
theorem power_series.coe_C {R : Type u} [semiring R] (r : R) :
( r) =
@[simp]
theorem power_series.coe_X {R : Type u} [semiring R] :
@[simp, norm_cast]
theorem power_series.coe_smul {R : Type u} [semiring R] {S : Type u_1} [semiring S] [ S] (r : R) (x : power_series S) :
(r x) = r x
@[simp, norm_cast]
theorem power_series.coe_bit0 {R : Type u} [semiring R] (f : power_series R) :
(bit0 f) =
@[simp, norm_cast]
theorem power_series.coe_bit1 {R : Type u} [semiring R] (f : power_series R) :
(bit1 f) =
@[simp, norm_cast]
theorem power_series.coe_pow {R : Type u} [semiring R] (f : power_series R) (n : ) :
(f ^ n) = f ^ n