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.

source

@[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 ℤ.

source

@[protected, instance]

noncomputable def laurent_series.has_coe {R : Type u} [semiring R] :

has_coe (power_series R) (laurent_series R)

Equations

laurent_series.has_coe = {coe := ⇑(hahn_series.of_power_series ℤ R)}

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

x.power_series_part = power_series.mk (λ (n : ℕ), x.coeff (hahn_series.order x + ↑n))

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

laurent_series.algebra = (hahn_series.of_power_series ℤ R).to_algebra

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