mathlib documentation

ring_theory.laurent_series

Laurent Series #

Main Definitions #

source
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 ℤ.

source
@[protected, instance]
noncomputable def laurent_series.has_coe {R : Type u} [semiring R] :
has_coe (power_series R) (laurent_series R)
Equations
source
theorem laurent_series.coe_power_series {R : Type u} [semiring R] (x : power_series R) :
↑x = ⇑(hahn_series.of_power_series ℤ R) x
source
@[simp]
theorem laurent_series.coeff_coe_power_series {R : Type u} [semiring R] (x : power_series R) (n : ℕ) :
↑x.coeff ↑n = ⇑(power_series.coeff R n) x
source
noncomputable def laurent_series.power_series_part {R : Type u} [semiring R] (x : laurent_series R) :
power_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
source
@[simp]
theorem laurent_series.power_series_part_coeff {R : Type u} [semiring R] (x : laurent_series R) (n : ℕ) :
⇑(power_series.coeff R n) x.power_series_part = x.coeff (hahn_series.order x + ↑n)
source
@[simp]
theorem laurent_series.power_series_part_zero {R : Type u} [semiring R] :
0.power_series_part = 0
source
@[simp]
theorem laurent_series.power_series_part_eq_zero {R : Type u} [semiring R] (x : laurent_series R) :
x.power_series_part = 0 ↔ x = 0
source
@[simp]
theorem laurent_series.single_order_mul_power_series_part {R : Type u} [semiring R] (x : laurent_series R) :
(⇑(hahn_series.single (hahn_series.order x)) 1) * ↑(x.power_series_part) = x
source
theorem laurent_series.of_power_series_power_series_part {R : Type u} [semiring R] (x : laurent_series R) :
⇑(hahn_series.of_power_series ℤ R) x.power_series_part = (⇑(hahn_series.single (-hahn_series.order x)) 1) * x
source
@[protected, instance]
noncomputable def laurent_series.algebra {R : Type u} [comm_semiring R] :
algebra (power_series R) (laurent_series R)
Equations
source
@[simp]
theorem laurent_series.coe_algebra_map {R : Type u} [comm_semiring R] :
⇑(algebra_map (power_series R) (laurent_series R)) = ⇑(hahn_series.of_power_series ℤ R)
source
@[protected, instance]
def laurent_series.of_power_series_localization {R : Type u} [comm_ring R] :
is_localization (submonoid.powers power_series.X) (laurent_series R)

The localization map from power series to Laurent series.

source
@[protected, instance]
def laurent_series.is_fraction_ring {K : Type u} [field K] :
is_fraction_ring (power_series K) (laurent_series K)
source
@[simp, norm_cast]
theorem power_series.coe_zero {R : Type u} [semiring R] :
↑0 = 0
source
@[simp, norm_cast]
theorem power_series.coe_one {R : Type u} [semiring R] :
↑1 = 1
source
@[simp, norm_cast]
theorem power_series.coe_add {R : Type u} [semiring R] (f g : power_series R) :
↑(f + g) = ↑f + ↑g
source
@[simp, norm_cast]
theorem power_series.coe_sub {R' : Type u_1} [ring R'] (f' g' : power_series R') :
↑(f' - g') = ↑f' - ↑g'
source
@[simp, norm_cast]
theorem power_series.coe_neg {R' : Type u_1} [ring R'] (f' : power_series R') :
↑-f' = -↑f'
source
@[simp, norm_cast]
theorem power_series.coe_mul {R : Type u} [semiring R] (f g : power_series R) :
↑f * g = (↑f) * ↑g
source
theorem power_series.coeff_coe {R : Type u} [semiring R] (f : power_series R) (i : ℤ) :
↑f.coeff i = ite (i < 0) 0 (⇑(power_series.coeff R i.nat_abs) f)
source
@[simp, norm_cast]
theorem power_series.coe_C {R : Type u} [semiring R] (r : R) :
↑(⇑(power_series.C R) r) = ⇑hahn_series.C r
source
@[simp]
theorem power_series.coe_X {R : Type u} [semiring R] :
↑power_series.X = ⇑(hahn_series.single 1) 1
source
@[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
source
@[simp, norm_cast]
theorem power_series.coe_bit0 {R : Type u} [semiring R] (f : power_series R) :
↑(bit0 f) = bit0 ↑f
source
@[simp, norm_cast]
theorem power_series.coe_bit1 {R : Type u} [semiring R] (f : power_series R) :
↑(bit1 f) = bit1 ↑f
source
@[simp, norm_cast]
theorem power_series.coe_pow {R : Type u} [semiring R] (f : power_series R) (n : ℕ) :
↑(f ^ n) = ↑f ^ n