mathlib documentation

ring_theory.hahn_series

Hahn Series #

If Γ is ordered and R has zero, then hahn_series Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on hahn_series Γ R, with the most studied case being when Γ is a linearly ordered abelian group and R is a field, in which case hahn_series Γ R is a valued field, with value group Γ.

These generalize Laurent series (with value group ), and Laurent series are implemented that way in the file ring_theory/laurent_series.

Main Definitions #

TODO #

References #

theorem hahn_series.ext {Γ : Type u_1} {R : Type u_2} {_inst_1 : partial_order Γ} {_inst_2 : has_zero R} (x y : hahn_series Γ R) (h : x.coeff = y.coeff) :
x = y
theorem hahn_series.ext_iff {Γ : Type u_1} {R : Type u_2} {_inst_1 : partial_order Γ} {_inst_2 : has_zero R} (x y : hahn_series Γ R) :
x = y x.coeff = y.coeff
@[ext]
structure hahn_series (Γ : Type u_1) (R : Type u_2) [partial_order Γ] [has_zero R] :
Type (max u_1 u_2)

If Γ is linearly ordered and R has zero, then hahn_series Γ R consists of formal series over Γ with coefficients in R, whose supports are well-founded.

Instances for hahn_series
@[simp]
theorem hahn_series.coeff_inj {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {x y : hahn_series Γ R} :
x.coeff = y.coeff x = y
def hahn_series.support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (x : hahn_series Γ R) :
set Γ

The support of a Hahn series is just the set of indices whose coefficients are nonzero. Notably, it is well-founded.

Equations
@[simp]
theorem hahn_series.is_pwo_support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (x : hahn_series Γ R) :
@[simp]
theorem hahn_series.is_wf_support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (x : hahn_series Γ R) :
@[simp]
theorem hahn_series.mem_support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (x : hahn_series Γ R) (a : Γ) :
a x.support x.coeff a 0
@[protected, instance]
def hahn_series.has_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] :
Equations
@[protected, instance]
def hahn_series.inhabited {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] :
Equations
@[protected, instance]
def hahn_series.subsingleton {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [subsingleton R] :
@[simp]
theorem hahn_series.zero_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} :
0.coeff a = 0
@[simp]
theorem hahn_series.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {x : hahn_series Γ R} :
x.coeff = 0 x = 0
theorem hahn_series.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {x : hahn_series Γ R} {g : Γ} (h : x.coeff g 0) :
x 0
@[simp]
theorem hahn_series.support_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] :
@[simp]
theorem hahn_series.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {x : hahn_series Γ R} :
@[simp]
theorem hahn_series.support_eq_empty_iff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {x : hahn_series Γ R} :
x.support = x = 0
noncomputable def hahn_series.single {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (a : Γ) :

single a r is the Hahn series which has coefficient r at a and zero otherwise.

Equations
@[simp]
theorem hahn_series.single_coeff_same {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (a : Γ) (r : R) :
@[simp]
theorem hahn_series.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a b : Γ} {r : R} (h : b a) :
theorem hahn_series.single_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a b : Γ} {r : R} :
((hahn_series.single a) r).coeff b = ite (b = a) r 0
@[simp]
theorem hahn_series.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} {r : R} (h : r 0) :
theorem hahn_series.support_single_subset {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} {r : R} :
theorem hahn_series.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} {r : R} {b : Γ} (h : b ((hahn_series.single a) r).support) :
b = a
@[simp]
theorem hahn_series.single_eq_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} :
theorem hahn_series.single_injective {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] (a : Γ) :
theorem hahn_series.single_ne_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} {r : R} (h : r 0) :
@[simp]
theorem hahn_series.single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} {r : R} :
@[protected, instance]
def hahn_series.nontrivial {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [nonempty Γ] [nontrivial R] :
noncomputable def hahn_series.order {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [has_zero Γ] (x : hahn_series Γ R) :
Γ

The order of a nonzero Hahn series x is a minimal element of Γ where x has a nonzero coefficient, the order of 0 is 0.

Equations
@[simp]
theorem hahn_series.order_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [has_zero Γ] :
0.order = 0
theorem hahn_series.order_of_ne {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [has_zero Γ] {x : hahn_series Γ R} (hx : x 0) :
x.order = _.min _
theorem hahn_series.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [has_zero Γ] {x : hahn_series Γ R} (hx : x 0) :
theorem hahn_series.order_le_of_coeff_ne_zero {R : Type u_2} [has_zero R] {Γ : Type u_1} [linear_ordered_cancel_add_comm_monoid Γ] {x : hahn_series Γ R} {g : Γ} (h : x.coeff g 0) :
@[simp]
theorem hahn_series.order_single {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {a : Γ} {r : R} [has_zero Γ] (h : r 0) :
theorem hahn_series.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] [has_zero Γ] {x : hahn_series Γ R} {i : Γ} (hi : i < x.order) :
x.coeff i = 0
noncomputable def hahn_series.emb_domain {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] (f : Γ ↪o Γ') :
hahn_series Γ Rhahn_series Γ' R

Extends the domain of a hahn_series by an order_embedding.

Equations
@[simp]
theorem hahn_series.emb_domain_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : hahn_series Γ R} {a : Γ} :
@[simp]
theorem hahn_series.emb_domain_mk_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ → Γ'} (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') {x : hahn_series Γ R} {a : Γ} :
(hahn_series.emb_domain {to_embedding := {to_fun := f, inj' := hfi}, map_rel_iff' := hf} x).coeff (f a) = x.coeff a
theorem hahn_series.emb_domain_notin_image_support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : hahn_series Γ R} {b : Γ'} (hb : b f '' x.support) :
theorem hahn_series.support_emb_domain_subset {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : hahn_series Γ R} :
theorem hahn_series.emb_domain_notin_range {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : hahn_series Γ R} {b : Γ'} (hb : b set.range f) :
@[simp]
theorem hahn_series.emb_domain_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} :
@[simp]
theorem hahn_series.emb_domain_single {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {g : Γ} {r : R} :
theorem hahn_series.emb_domain_injective {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} :
@[protected, instance]
def hahn_series.has_add {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] :
Equations
@[protected, instance]
def hahn_series.add_monoid {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] :
Equations
@[simp]
theorem hahn_series.add_coeff' {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] {x y : hahn_series Γ R} :
(x + y).coeff = x.coeff + y.coeff
theorem hahn_series.add_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] {x y : hahn_series Γ R} {a : Γ} :
(x + y).coeff a = x.coeff a + y.coeff a
theorem hahn_series.support_add_subset {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] {x y : hahn_series Γ R} :
theorem hahn_series.min_order_le_order_add {R : Type u_2} [add_monoid R] {Γ : Type u_1} [linear_ordered_cancel_add_comm_monoid Γ] {x y : hahn_series Γ R} (hxy : x + y 0) :
@[simp]
theorem hahn_series.single.add_monoid_hom_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] (a : Γ) (ᾰ : R) :
noncomputable def hahn_series.single.add_monoid_hom {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] (a : Γ) :

single as an additive monoid/group homomorphism

Equations
@[simp]
theorem hahn_series.coeff.add_monoid_hom_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] (g : Γ) (f : hahn_series Γ R) :
def hahn_series.coeff.add_monoid_hom {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] (g : Γ) :

coeff g as an additive monoid/group homomorphism

Equations
theorem hahn_series.emb_domain_add {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_monoid R] {Γ' : Type u_3} [partial_order Γ'] (f : Γ ↪o Γ') (x y : hahn_series Γ R) :
@[protected, instance]
def hahn_series.add_group {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_group R] :
Equations
@[simp]
theorem hahn_series.neg_coeff' {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_group R] {x : hahn_series Γ R} :
theorem hahn_series.neg_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_group R] {x : hahn_series Γ R} {a : Γ} :
(-x).coeff a = -x.coeff a
@[simp]
theorem hahn_series.support_neg {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_group R] {x : hahn_series Γ R} :
@[simp]
theorem hahn_series.sub_coeff' {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_group R] {x y : hahn_series Γ R} :
(x - y).coeff = x.coeff - y.coeff
theorem hahn_series.sub_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_group R] {x y : hahn_series Γ R} {a : Γ} :
(x - y).coeff a = x.coeff a - y.coeff a
@[protected, instance]
def hahn_series.has_smul {Γ : Type u_1} {R : Type u_2} [partial_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] :
Equations
@[simp]
theorem hahn_series.smul_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] {r : R} {x : hahn_series Γ V} {a : Γ} :
(r x).coeff a = r x.coeff a
@[protected, instance]
def hahn_series.distrib_mul_action {Γ : Type u_1} {R : Type u_2} [partial_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] :
Equations
@[protected, instance]
def hahn_series.is_scalar_tower {Γ : Type u_1} {R : Type u_2} [partial_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] {S : Type u_4} [monoid S] [distrib_mul_action S V] [has_smul R S] [is_scalar_tower R S V] :
@[protected, instance]
def hahn_series.smul_comm_class {Γ : Type u_1} {R : Type u_2} [partial_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] {S : Type u_4} [monoid S] [distrib_mul_action S V] [smul_comm_class R S V] :
@[protected, instance]
def hahn_series.module {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] {V : Type u_3} [add_comm_monoid V] [module R V] :
Equations
@[simp]
theorem hahn_series.single.linear_map_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] (a : Γ) (ᾰ : R) :
noncomputable def hahn_series.single.linear_map {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] (a : Γ) :

single as a linear map

Equations
def hahn_series.coeff.linear_map {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] (g : Γ) :

coeff g as a linear map

Equations
@[simp]
theorem hahn_series.coeff.linear_map_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] (g : Γ) (ᾰ : hahn_series Γ R) :
theorem hahn_series.emb_domain_smul {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] {Γ' : Type u_4} [partial_order Γ'] (f : Γ ↪o Γ') (r : R) (x : hahn_series Γ R) :
@[simp]
theorem hahn_series.emb_domain_linear_map_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] {Γ' : Type u_4} [partial_order Γ'] (f : Γ ↪o Γ') (ᾰ : hahn_series Γ R) :
noncomputable def hahn_series.emb_domain_linear_map {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [semiring R] {Γ' : Type u_4} [partial_order Γ'] (f : Γ ↪o Γ') :

Extending the domain of Hahn series is a linear map.

Equations
@[protected, instance]
noncomputable def hahn_series.has_one {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [has_zero R] [has_one R] :
Equations
@[simp]
theorem hahn_series.one_coeff {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [has_zero R] [has_one R] {a : Γ} :
1.coeff a = ite (a = 0) 1 0
@[simp]
theorem hahn_series.single_zero_one {R : Type u_2} [has_zero R] [has_one R] :
@[simp]
theorem hahn_series.support_one {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [mul_zero_one_class R] [nontrivial R] :
1.support = {0}
@[simp]
theorem hahn_series.order_one {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [mul_zero_one_class R] :
1.order = 0
@[protected, instance]
noncomputable def hahn_series.has_mul {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] :
Equations
@[simp]
theorem hahn_series.mul_coeff {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {x y : hahn_series Γ R} {a : Γ} :
(x * y).coeff a = (finset.add_antidiagonal _ _ a).sum (λ (ij : Γ × Γ), x.coeff ij.fst * y.coeff ij.snd)
theorem hahn_series.mul_coeff_right' {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {x y : hahn_series Γ R} {a : Γ} {s : set Γ} (hs : s.is_pwo) (hys : y.support s) :
(x * y).coeff a = (finset.add_antidiagonal _ hs a).sum (λ (ij : Γ × Γ), x.coeff ij.fst * y.coeff ij.snd)
theorem hahn_series.mul_coeff_left' {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {x y : hahn_series Γ R} {a : Γ} {s : set Γ} (hs : s.is_pwo) (hxs : x.support s) :
(x * y).coeff a = (finset.add_antidiagonal hs _ a).sum (λ (ij : Γ × Γ), x.coeff ij.fst * y.coeff ij.snd)
theorem hahn_series.single_mul_coeff_add {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {r : R} {x : hahn_series Γ R} {a b : Γ} :
((hahn_series.single b) r * x).coeff (a + b) = r * x.coeff a
theorem hahn_series.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {r : R} {x : hahn_series Γ R} {a b : Γ} :
(x * (hahn_series.single b) r).coeff (a + b) = x.coeff a * r
@[simp]
theorem hahn_series.mul_single_zero_coeff {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {r : R} {x : hahn_series Γ R} {a : Γ} :
(x * (hahn_series.single 0) r).coeff a = x.coeff a * r
theorem hahn_series.single_zero_mul_coeff {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {r : R} {x : hahn_series Γ R} {a : Γ} :
((hahn_series.single 0) r * x).coeff a = r * x.coeff a
@[simp]
theorem hahn_series.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} :
@[protected, instance]
noncomputable def hahn_series.semiring {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] :
Equations
@[protected, instance]
noncomputable def hahn_series.non_assoc_ring {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_ring R] :
Equations
@[protected, instance]
noncomputable def hahn_series.ring {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [ring R] :
Equations
@[protected, instance]
def hahn_series.is_domain {R : Type u_2} {Γ : Type u_1} [linear_ordered_cancel_add_comm_monoid Γ] [ring R] [is_domain R] :
@[simp]
theorem hahn_series.order_mul {R : Type u_2} {Γ : Type u_1} [linear_ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] [no_zero_divisors R] {x y : hahn_series Γ R} (hx : x 0) (hy : y 0) :
(x * y).order = x.order + y.order
@[simp]
theorem hahn_series.order_pow {R : Type u_2} {Γ : Type u_1} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] [no_zero_divisors R] (x : hahn_series Γ R) (n : ) :
(x ^ n).order = n x.order
@[simp]
theorem hahn_series.single_mul_single {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_unital_non_assoc_semiring R] {a b : Γ} {r s : R} :
@[simp]
theorem hahn_series.C_apply {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_semiring R] (ᾰ : R) :
noncomputable def hahn_series.C {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_semiring R] :

C a is the constant Hahn Series a. C is provided as a ring homomorphism.

Equations
@[simp]
theorem hahn_series.C_zero {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_semiring R] :
@[simp]
theorem hahn_series.C_one {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_semiring R] :
theorem hahn_series.C_ne_zero {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_semiring R] {r : R} (h : r 0) :
theorem hahn_series.order_C {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [non_assoc_semiring R] {r : R} :
theorem hahn_series.C_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} :
theorem hahn_series.emb_domain_mul {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] {Γ' : Type u_3} [ordered_cancel_add_comm_monoid Γ'] [non_unital_non_assoc_semiring R] (f : Γ ↪o Γ') (hf : ∀ (x y : Γ), f (x + y) = f x + f y) (x y : hahn_series Γ R) :
theorem hahn_series.emb_domain_one {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] {Γ' : Type u_3} [ordered_cancel_add_comm_monoid Γ'] [non_assoc_semiring R] (f : Γ ↪o Γ') (hf : f 0 = 0) :
noncomputable def hahn_series.emb_domain_ring_hom {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] {Γ' : Type u_3} [ordered_cancel_add_comm_monoid Γ'] [non_assoc_semiring R] (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') :

Extending the domain of Hahn series is a ring homomorphism.

Equations
@[simp]
theorem hahn_series.emb_domain_ring_hom_apply {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] {Γ' : Type u_3} [ordered_cancel_add_comm_monoid Γ'] [non_assoc_semiring R] (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') (ᾰ : hahn_series Γ R) :
theorem hahn_series.emb_domain_ring_hom_C {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] {Γ' : Type u_3} [ordered_cancel_add_comm_monoid Γ'] [non_assoc_semiring R] {f : Γ →+ Γ'} {hfi : function.injective f} {hf : ∀ (g g' : Γ), f g f g' g g'} {r : R} :
@[protected, instance]
noncomputable def hahn_series.algebra {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] :
Equations
theorem hahn_series.algebra_map_apply {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] {r : R} :
@[protected, instance]
@[simp]
theorem hahn_series.emb_domain_alg_hom_apply {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] {Γ' : Type u_4} [ordered_cancel_add_comm_monoid Γ'] (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') (ᾰ : hahn_series Γ A) :
noncomputable def hahn_series.emb_domain_alg_hom {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] {Γ' : Type u_4} [ordered_cancel_add_comm_monoid Γ'] (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') :

Extending the domain of Hahn series is an algebra homomorphism.

Equations
noncomputable def hahn_series.to_power_series {R : Type u_2} [semiring R] :

The ring hahn_series ℕ R is isomorphic to power_series R.

Equations
noncomputable def hahn_series.of_power_series (Γ : Type u_1) (R : Type u_2) [semiring R] [ordered_semiring Γ] [nontrivial Γ] :

Casts a power series as a Hahn series with coefficients from an ordered_semiring.

Equations
theorem hahn_series.of_power_series_apply_coeff {Γ : Type u_1} {R : Type u_2} [semiring R] [ordered_semiring Γ] [nontrivial Γ] (x : power_series R) (n : ) :
@[simp]
theorem hahn_series.of_power_series_C {Γ : Type u_1} {R : Type u_2} [semiring R] [ordered_semiring Γ] [nontrivial Γ] (r : R) :
@[simp]
theorem hahn_series.to_mv_power_series_apply {R : Type u_2} [semiring R] {σ : Type u_1} [fintype σ] (f : hahn_series →₀ ) R) (ᾰ : σ →₀ ) :
def hahn_series.to_mv_power_series {R : Type u_2} [semiring R] {σ : Type u_1} [fintype σ] :

The ring hahn_series (σ →₀ ℕ) R is isomorphic to mv_power_series σ R for a fintype σ. We take the index set of the hahn series to be finsupp rather than pi, even though we assume fintype σ as this is more natural for alignment with mv_power_series. After importing algebra.order.pi the ring hahn_series (σ → ℕ) R could be constructed instead.

Equations
@[simp]
theorem hahn_series.coeff_to_mv_power_series {R : Type u_2} [semiring R] {σ : Type u_3} [fintype σ] {f : hahn_series →₀ ) R} {n : σ →₀ } :
noncomputable def hahn_series.to_power_series_alg (R : Type u_2) [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] :

The R-algebra hahn_series ℕ A is isomorphic to power_series A.

Equations
noncomputable def hahn_series.of_power_series_alg (Γ : Type u_1) (R : Type u_2) [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] [ordered_semiring Γ] [nontrivial Γ] :

Casting a power series as a Hahn series with coefficients from an ordered_semiring is an algebra homomorphism.

Equations
@[simp]
theorem hahn_series.of_power_series_alg_apply_coeff (Γ : Type u_1) (R : Type u_2) [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] [ordered_semiring Γ] [nontrivial Γ] (ᾰ : power_series A) (b : Γ) :
((hahn_series.of_power_series_alg Γ R) ᾰ).coeff b = dite (∃ (a : ), ¬(power_series.coeff A a) = 0 a = b) (λ (h : ∃ (a : ), ¬(power_series.coeff A a) = 0 a = b), (power_series.coeff A (classical.some _)) ᾰ) (λ (h : ¬∃ (a : ), ¬(power_series.coeff A a) = 0 a = b), 0)
@[protected, instance]
noncomputable def hahn_series.power_series_algebra (Γ : Type u_1) (R : Type u_2) [comm_semiring R] [ordered_semiring Γ] [nontrivial Γ] {S : Type u_3} [comm_semiring S] [algebra S (power_series R)] :
Equations
theorem hahn_series.algebra_map_apply' (Γ : Type u_1) {R : Type u_2} [comm_semiring R] [ordered_semiring Γ] [nontrivial Γ] {S : Type u_4} [comm_semiring S] [algebra S (power_series R)] (x : S) :
noncomputable def hahn_series.add_val (Γ : Type u_1) (R : Type u_2) [linear_ordered_add_comm_group Γ] [ring R] [is_domain R] :

The additive valuation on hahn_series Γ R, returning the smallest index at which a Hahn Series has a nonzero coefficient, or for the 0 series.

Equations
theorem hahn_series.add_val_apply {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [ring R] [is_domain R] {x : hahn_series Γ R} :
@[simp]
theorem hahn_series.add_val_apply_of_ne {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [ring R] [is_domain R] {x : hahn_series Γ R} (hx : x 0) :
theorem hahn_series.add_val_le_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [ring R] [is_domain R] {x : hahn_series Γ R} {g : Γ} (h : x.coeff g 0) :
theorem hahn_series.is_pwo_Union_support_powers {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [ring R] [is_domain R] {x : hahn_series Γ R} (hx : 0 < (hahn_series.add_val Γ R) x) :
(⋃ (n : ), (x ^ n).support).is_pwo
structure hahn_series.summable_family (Γ : Type u_1) (R : Type u_2) [partial_order Γ] [add_comm_monoid R] (α : Type u_3) :
Type (max u_1 u_2 u_3)

An infinite family of Hahn series which has a formal coefficient-wise sum. The requirements for this are that the union of the supports of the series is well-founded, and that only finitely many series are nonzero at any given coefficient.

Instances for hahn_series.summable_family
@[protected, instance]
def hahn_series.summable_family.has_coe_to_fun {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
theorem hahn_series.summable_family.is_pwo_Union_support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} (s : hahn_series.summable_family Γ R α) :
(⋃ (a : α), (s a).support).is_pwo
theorem hahn_series.summable_family.finite_co_support {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} (s : hahn_series.summable_family Γ R α) (g : Γ) :
(function.support (λ (a : α), (s a).coeff g)).finite
theorem hahn_series.summable_family.coe_injective {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
@[ext]
theorem hahn_series.summable_family.ext {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} (h : ∀ (a : α), s a = t a) :
s = t
@[protected, instance]
def hahn_series.summable_family.has_add {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
@[protected, instance]
def hahn_series.summable_family.has_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
@[protected, instance]
def hahn_series.summable_family.inhabited {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.coe_add {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} :
(s + t) = s + t
theorem hahn_series.summable_family.add_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} {a : α} :
(s + t) a = s a + t a
@[simp]
theorem hahn_series.summable_family.coe_zero {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
0 = 0
theorem hahn_series.summable_family.zero_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {a : α} :
0 a = 0
@[protected, instance]
def hahn_series.summable_family.add_comm_monoid {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
noncomputable def hahn_series.summable_family.hsum {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} (s : hahn_series.summable_family Γ R α) :

The infinite sum of a summable_family of Hahn series.

Equations
@[simp]
theorem hahn_series.summable_family.hsum_coeff {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} {g : Γ} :
s.hsum.coeff g = finsum (λ (i : α), (s i).coeff g)
theorem hahn_series.summable_family.support_hsum_subset {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} :
s.hsum.support ⋃ (a : α), (s a).support
@[simp]
theorem hahn_series.summable_family.hsum_add {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} :
(s + t).hsum = s.hsum + t.hsum
@[protected, instance]
def hahn_series.summable_family.add_comm_group {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_group R] {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.coe_neg {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_group R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} :
theorem hahn_series.summable_family.neg_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_group R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} {a : α} :
(-s) a = -s a
@[simp]
theorem hahn_series.summable_family.coe_sub {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_group R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} :
(s - t) = s - t
theorem hahn_series.summable_family.sub_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_group R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} {a : α} :
(s - t) a = s a - t a
@[protected, instance]
noncomputable def hahn_series.summable_family.has_smul {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.smul_apply {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] {α : Type u_3} {x : hahn_series Γ R} {s : hahn_series.summable_family Γ R α} {a : α} :
(x s) a = x * s a
@[simp]
theorem hahn_series.summable_family.hsum_smul {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] {α : Type u_3} {x : hahn_series Γ R} {s : hahn_series.summable_family Γ R α} :
(x s).hsum = x * s.hsum
@[simp]
noncomputable def hahn_series.summable_family.lsum {Γ : Type u_1} {R : Type u_2} [ordered_cancel_add_comm_monoid Γ] [semiring R] {α : Type u_3} :

The summation of a summable_family as a linear_map.

Equations
@[simp]
theorem hahn_series.summable_family.hsum_sub {Γ : Type u_1} [ordered_cancel_add_comm_monoid Γ] {α : Type u_3} {R : Type u_2} [ring R] {s t : hahn_series.summable_family Γ R α} :
(s - t).hsum = s.hsum - t.hsum
def hahn_series.summable_family.of_finsupp {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} (f : α →₀ hahn_series Γ R) :

A family with only finitely many nonzero elements is summable.

Equations
@[simp]
theorem hahn_series.summable_family.coe_of_finsupp {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {f : α →₀ hahn_series Γ R} :
@[simp]
theorem hahn_series.summable_family.hsum_of_finsupp {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {f : α →₀ hahn_series Γ R} :
noncomputable def hahn_series.summable_family.emb_domain {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {β : Type u_4} (s : hahn_series.summable_family Γ R α) (f : α β) :

A summable family can be reindexed by an embedding without changing its sum.

Equations
theorem hahn_series.summable_family.emb_domain_apply {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {β : Type u_4} (s : hahn_series.summable_family Γ R α) (f : α β) {b : β} :
(s.emb_domain f) b = dite (b set.range f) (λ (h : b set.range f), s (classical.some h)) (λ (h : b set.range f), 0)
@[simp]
theorem hahn_series.summable_family.emb_domain_image {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {β : Type u_4} (s : hahn_series.summable_family Γ R α) (f : α β) {a : α} :
(s.emb_domain f) (f a) = s a
@[simp]
theorem hahn_series.summable_family.emb_domain_notin_range {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {β : Type u_4} (s : hahn_series.summable_family Γ R α) (f : α β) {b : β} (h : b set.range f) :
(s.emb_domain f) b = 0
@[simp]
theorem hahn_series.summable_family.hsum_emb_domain {Γ : Type u_1} {R : Type u_2} [partial_order Γ] [add_comm_monoid R] {α : Type u_3} {β : Type u_4} (s : hahn_series.summable_family Γ R α) (f : α β) :
noncomputable def hahn_series.summable_family.powers {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [comm_ring R] [is_domain R] (x : hahn_series Γ R) (hx : 0 < (hahn_series.add_val Γ R) x) :

The powers of an element of positive valuation form a summable family.

Equations
theorem hahn_series.unit_aux {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [comm_ring R] [is_domain R] (x : hahn_series Γ R) {r : R} (hr : r * x.coeff x.order = 1) :
theorem hahn_series.is_unit_iff {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [comm_ring R] [is_domain R] {x : hahn_series Γ R} :
@[protected, instance]
noncomputable def hahn_series.field {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [field R] :
Equations