mathlib documentation

ring_theory.laurent_series

Laurent Series #

Main Definitions #

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 : ) :
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} [comm_semiring R] :
Equations
@[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 : ) :
@[simp, norm_cast]
theorem power_series.coe_C {R : Type u} [semiring R] (r : R) :
@[simp]
@[simp, norm_cast]
theorem power_series.coe_smul {R : Type u} [semiring R] {S : Type u_1} [semiring S] [module R 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) :
@[simp, norm_cast]
theorem power_series.coe_bit1 {R : Type u} [semiring R] (f : power_series R) :
@[simp, norm_cast]
theorem power_series.coe_pow {R : Type u} [semiring R] (f : power_series R) (n : ) :
(f ^ n) = f ^ n