# mathlibdocumentation

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 #

• 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.
• If `R` is a (commutative) additive monoid or group, then so is `hahn_series Γ R`.
• If `R` is a (comm_)(semi)ring, then so is `hahn_series Γ R`.
• `hahn_series.add_val Γ R` defines an `add_valuation` on `hahn_series Γ R` when `Γ` is linearly ordered.
• A `hahn_series.summable_family` is a family of Hahn series such that the union of their supports is well-founded and only finitely many are nonzero at any given coefficient. They have a formal sum, `hahn_series.summable_family.hsum`, which can be bundled as a `linear_map` as `hahn_series.summable_family.lsum`. Note that this is different from `summable` in the valuation topology, because there are topologically summable families that do not satisfy the axioms of `hahn_series.summable_family`, and formally summable families whose sums do not converge topologically.
• Laurent series over `R` are implemented as `hahn_series ℤ R` in the file `ring_theory/laurent_series`.

## TODO #

• Build an API for the variable `X` (defined to be `single 1 1 : hahn_series Γ R`) in analogy to `X : R[X]` and `X : power_series R`

## References #

theorem hahn_series.ext {Γ : Type u_1} {R : Type u_2} {_inst_1 : partial_order Γ} {_inst_2 : has_zero R} (x y : 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 : R) :
x = y x.coeff = y.coeff
@[ext]
structure hahn_series (Γ : Type u_1) (R : Type u_2) [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`
theorem hahn_series.coeff_injective {Γ : Type u_1} {R : Type u_2} [has_zero R] :
@[simp]
theorem hahn_series.coeff_inj {Γ : Type u_1} {R : Type u_2} [has_zero R] {x y : R} :
x.coeff = y.coeff x = y
def hahn_series.support {Γ : Type u_1} {R : Type u_2} [has_zero R] (x : 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} [has_zero R] (x : R) :
@[simp]
theorem hahn_series.is_wf_support {Γ : Type u_1} {R : Type u_2} [has_zero R] (x : R) :
@[simp]
theorem hahn_series.mem_support {Γ : Type u_1} {R : Type u_2} [has_zero R] (x : R) (a : Γ) :
a x.support x.coeff a 0
@[protected, instance]
def hahn_series.has_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] :
Equations
@[protected, instance]
def hahn_series.inhabited {Γ : Type u_1} {R : Type u_2} [has_zero R] :
Equations
@[protected, instance]
def hahn_series.subsingleton {Γ : Type u_1} {R : Type u_2} [has_zero R] [subsingleton R] :
@[simp]
theorem hahn_series.zero_coeff {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} :
0.coeff a = 0
@[simp]
theorem hahn_series.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [has_zero R] {x : R} :
x.coeff = 0 x = 0
theorem hahn_series.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] {x : R} {g : Γ} (h : x.coeff g 0) :
x 0
@[simp]
theorem hahn_series.support_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] :
@[simp]
theorem hahn_series.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [has_zero R] {x : R} :
@[simp]
theorem hahn_series.support_eq_empty_iff {Γ : Type u_1} {R : Type u_2} [has_zero R] {x : R} :
x = 0
noncomputable def hahn_series.single {Γ : Type u_1} {R : Type u_2} [has_zero R] (a : Γ) :
R)

`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} [has_zero R] (a : Γ) (r : R) :
( r).coeff a = r
@[simp]
theorem hahn_series.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [has_zero R] {a b : Γ} {r : R} (h : b a) :
( r).coeff b = 0
theorem hahn_series.single_coeff {Γ : Type u_1} {R : Type u_2} [has_zero R] {a b : Γ} {r : R} :
( r).coeff b = ite (b = a) r 0
@[simp]
theorem hahn_series.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} {r : R} (h : r 0) :
( r).support = {a}
theorem hahn_series.support_single_subset {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} {r : R} :
( r).support {a}
theorem hahn_series.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} {r : R} {b : Γ} (h : b ( r).support) :
b = a
@[simp]
theorem hahn_series.single_eq_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} :
0 = 0
theorem hahn_series.single_injective {Γ : Type u_1} {R : Type u_2} [has_zero R] (a : Γ) :
theorem hahn_series.single_ne_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} {r : R} (h : r 0) :
r 0
@[simp]
theorem hahn_series.single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} {r : R} :
r = 0 r = 0
@[protected, instance]
def hahn_series.nontrivial {Γ : Type u_1} {R : Type u_2} [has_zero R] [nonempty Γ] [nontrivial R] :
noncomputable def hahn_series.order {Γ : Type u_1} {R : Type u_2} [has_zero R] [has_zero Γ] (x : 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} [has_zero R] [has_zero Γ] :
0.order = 0
theorem hahn_series.order_of_ne {Γ : Type u_1} {R : Type u_2} [has_zero R] [has_zero Γ] {x : R} (hx : x 0) :
x.order = _.min _
theorem hahn_series.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] [has_zero Γ] {x : R} (hx : x 0) :
theorem hahn_series.order_le_of_coeff_ne_zero {R : Type u_2} [has_zero R] {Γ : Type u_1} {x : R} {g : Γ} (h : x.coeff g 0) :
@[simp]
theorem hahn_series.order_single {Γ : Type u_1} {R : Type u_2} [has_zero R] {a : Γ} {r : R} [has_zero Γ] (h : r 0) :
( r).order = a
theorem hahn_series.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_2} [has_zero R] [has_zero Γ] {x : R} {i : Γ} (hi : i < x.order) :
x.coeff i = 0
noncomputable def hahn_series.emb_domain {Γ : Type u_1} {R : Type u_2} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] (f : Γ ↪o Γ') :
R 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} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : R} {a : Γ} :
.coeff (f a) = x.coeff a
@[simp]
theorem hahn_series.emb_domain_mk_coeff {Γ : Type u_1} {R : Type u_2} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ → Γ'} (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') {x : 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} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : R} {b : Γ'} (hb : b f '' x.support) :
.coeff b = 0
theorem hahn_series.support_emb_domain_subset {Γ : Type u_1} {R : Type u_2} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : R} :
theorem hahn_series.emb_domain_notin_range {Γ : Type u_1} {R : Type u_2} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} {x : R} {b : Γ'} (hb : b ) :
.coeff b = 0
@[simp]
theorem hahn_series.emb_domain_zero {Γ : Type u_1} {R : Type u_2} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} :
@[simp]
theorem hahn_series.emb_domain_single {Γ : Type u_1} {R : Type u_2} [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} [has_zero R] {Γ' : Type u_3} [partial_order Γ'] {f : Γ ↪o Γ'} :
@[protected, instance]
def hahn_series.has_add {Γ : Type u_1} {R : Type u_2} [add_monoid R] :
Equations
@[protected, instance]
def hahn_series.add_monoid {Γ : Type u_1} {R : Type u_2} [add_monoid R] :
Equations
@[simp]
theorem hahn_series.add_coeff' {Γ : Type u_1} {R : Type u_2} [add_monoid R] {x y : R} :
(x + y).coeff = x.coeff + y.coeff
theorem hahn_series.add_coeff {Γ : Type u_1} {R : Type u_2} [add_monoid R] {x y : 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} [add_monoid R] {x y : R} :
theorem hahn_series.min_order_le_order_add {R : Type u_2} [add_monoid R] {Γ : Type u_1} {x y : R} (hxy : x + y 0) :
(x + y).order
@[simp]
theorem hahn_series.single.add_monoid_hom_apply {Γ : Type u_1} {R : Type u_2} [add_monoid R] (a : Γ) (ᾰ : R) :
noncomputable def hahn_series.single.add_monoid_hom {Γ : Type u_1} {R : Type u_2} [add_monoid R] (a : Γ) :
R →+ R

`single` as an additive monoid/group homomorphism

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

`coeff g` as an additive monoid/group homomorphism

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

`single` as a linear map

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

`coeff g` as a linear map

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

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} [has_zero R] [has_one R] :
Equations
@[simp]
theorem hahn_series.one_coeff {Γ : Type u_1} {R : Type u_2} [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] :
1 = 1
@[simp]
theorem hahn_series.support_one {Γ : Type u_1} {R : Type u_2} [nontrivial R] :
1.support = {0}
@[simp]
theorem hahn_series.order_one {Γ : Type u_1} {R : Type u_2}  :
1.order = 0
@[protected, instance]
noncomputable def hahn_series.has_mul {Γ : Type u_1} {R : Type u_2}  :
Equations
@[simp]
theorem hahn_series.mul_coeff {Γ : Type u_1} {R : Type u_2} {x y : R} {a : Γ} :
(x * y).coeff a = a).sum (λ (ij : Γ × Γ), x.coeff ij.fst * y.coeff ij.snd)
theorem hahn_series.mul_coeff_right' {Γ : Type u_1} {R : Type u_2} {x y : R} {a : Γ} {s : set Γ} (hs : s.is_pwo) (hys : y.support s) :
(x * y).coeff a = a).sum (λ (ij : Γ × Γ), x.coeff ij.fst * y.coeff ij.snd)
theorem hahn_series.mul_coeff_left' {Γ : Type u_1} {R : Type u_2} {x y : R} {a : Γ} {s : set Γ} (hs : s.is_pwo) (hxs : x.support s) :
(x * y).coeff a = a).sum (λ (ij : Γ × Γ), x.coeff ij.fst * y.coeff ij.snd)
@[protected, instance]
noncomputable def hahn_series.distrib {Γ : Type u_1} {R : Type u_2}  :
Equations
theorem hahn_series.single_mul_coeff_add {Γ : Type u_1} {R : Type u_2} {r : R} {x : R} {a b : Γ} :
( r * x).coeff (a + b) = r * x.coeff a
theorem hahn_series.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} {r : R} {x : R} {a b : Γ} :
(x * r).coeff (a + b) = x.coeff a * r
@[simp]
theorem hahn_series.mul_single_zero_coeff {Γ : Type u_1} {R : Type u_2} {r : R} {x : R} {a : Γ} :
(x * r).coeff a = x.coeff a * r
theorem hahn_series.single_zero_mul_coeff {Γ : Type u_1} {R : Type u_2} {r : R} {x : R} {a : Γ} :
( r * x).coeff a = r * x.coeff a
@[simp]
theorem hahn_series.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [semiring R] {r : R} {x : R} :
r * x = r x
theorem hahn_series.support_mul_subset_add_support {Γ : Type u_1} {R : Type u_2} {x y : R} :
theorem hahn_series.mul_coeff_order_add_order {R : Type u_2} {Γ : Type u_1} (x y : R) :
(x * y).coeff (x.order + y.order) = x.coeff x.order * y.coeff y.order
@[protected, instance]
noncomputable def hahn_series.non_unital_non_assoc_semiring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.non_unital_semiring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.non_assoc_semiring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.semiring {Γ : Type u_1} {R : Type u_2} [semiring R] :
Equations
@[protected, instance]
noncomputable def hahn_series.non_unital_comm_semiring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.comm_semiring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.non_unital_non_assoc_ring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.non_unital_ring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.non_assoc_ring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.ring {Γ : Type u_1} {R : Type u_2} [ring R] :
ring R)
Equations
@[protected, instance]
noncomputable def hahn_series.non_unital_comm_ring {Γ : Type u_1} {R : Type u_2}  :
Equations
@[protected, instance]
noncomputable def hahn_series.comm_ring {Γ : Type u_1} {R : Type u_2} [comm_ring R] :
Equations
@[protected, instance]
def hahn_series.no_zero_divisors {R : Type u_2} {Γ : Type u_1}  :
@[protected, instance]
def hahn_series.is_domain {R : Type u_2} {Γ : Type u_1} [ring R] [is_domain R] :
@[simp]
theorem hahn_series.order_mul {R : Type u_2} {Γ : Type u_1} {x y : 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} [semiring R] (x : R) (n : ) :
(x ^ n).order = n x.order
@[simp]
theorem hahn_series.single_mul_single {Γ : Type u_1} {R : Type u_2} {a b : Γ} {r s : R} :
r * s = (hahn_series.single (a + b)) (r * s)
@[simp]
theorem hahn_series.C_apply {Γ : Type u_1} {R : Type u_2} (ᾰ : R) :
noncomputable def hahn_series.C {Γ : Type u_1} {R : Type u_2}  :
R →+* 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}  :
@[simp]
theorem hahn_series.C_one {Γ : Type u_1} {R : Type u_2}  :
theorem hahn_series.C_injective {Γ : Type u_1} {R : Type u_2}  :
theorem hahn_series.C_ne_zero {Γ : Type u_1} {R : Type u_2} {r : R} (h : r 0) :
theorem hahn_series.order_C {Γ : Type u_1} {R : Type u_2} {r : R} :
.order = 0
theorem hahn_series.C_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [semiring R] {r : R} {x : R} :
= r x
theorem hahn_series.emb_domain_mul {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} (f : Γ ↪o Γ') (hf : ∀ (x y : Γ), f (x + y) = f x + f y) (x y : R) :
(x * y) =
theorem hahn_series.emb_domain_one {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} (f : Γ ↪o Γ') (hf : f 0 = 0) :
noncomputable def hahn_series.emb_domain_ring_hom {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') :
R →+* R

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} {Γ' : Type u_3} (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') (ᾰ : R) :
theorem hahn_series.emb_domain_ring_hom_C {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} {f : Γ →+ Γ'} {hfi : function.injective f} {hf : ∀ (g g' : Γ), f g f g' g g'} {r : R} :
hf) =
@[protected, instance]
noncomputable def hahn_series.algebra {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] :
A)
Equations
theorem hahn_series.C_eq_algebra_map {Γ : Type u_1} {R : Type u_2}  :
theorem hahn_series.algebra_map_apply {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] {r : R} :
A)) r = hahn_series.C ( A) r)
@[protected, instance]
def hahn_series.subalgebra.nontrivial {Γ : Type u_1} {R : Type u_2} [nontrivial Γ] [nontrivial R] :
@[simp]
theorem hahn_series.emb_domain_alg_hom_apply {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] {Γ' : Type u_4} (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') (ᾰ : A) :
hf) = hf).to_fun
noncomputable def hahn_series.emb_domain_alg_hom {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [semiring A] [ A] {Γ' : Type u_4} (f : Γ →+ Γ') (hfi : function.injective f) (hf : ∀ (g g' : Γ), f g f g' g g') :
A →ₐ[R] A

Extending the domain of Hahn series is an algebra homomorphism.

Equations
@[simp]
theorem hahn_series.to_power_series_symm_apply_coeff {R : Type u_2} [semiring R] (f : power_series R) (n : ) :
= n) f
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
@[simp]
theorem hahn_series.to_power_series_apply {R : Type u_2} [semiring R] (f : R) :
theorem hahn_series.coeff_to_power_series {R : Type u_2} [semiring R] {f : R} {n : } :
= f.coeff n
theorem hahn_series.coeff_to_power_series_symm {R : Type u_2} [semiring R] {f : power_series R} {n : } :
= n) f
noncomputable def hahn_series.of_power_series (Γ : Type u_1) (R : Type u_2) [semiring R] [nontrivial Γ] :

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

Equations
theorem hahn_series.of_power_series_injective {Γ : Type u_1} {R : Type u_2} [semiring R] [nontrivial Γ] :
@[simp]
theorem hahn_series.of_power_series_apply {Γ : Type u_1} {R : Type u_2} [semiring R] [nontrivial Γ] (x : power_series R) :
theorem hahn_series.of_power_series_apply_coeff {Γ : Type u_1} {R : Type u_2} [semiring R] [nontrivial Γ] (x : power_series R) (n : ) :
( x).coeff n = n) x
@[simp]
theorem hahn_series.of_power_series_C {Γ : Type u_1} {R : Type u_2} [semiring R] [nontrivial Γ] (r : R) :
( r) =
@[simp]
theorem hahn_series.of_power_series_X {Γ : Type u_1} {R : Type u_2} [semiring R] [nontrivial Γ] :
@[simp]
theorem hahn_series.of_power_series_X_pow {Γ : Type u_1} [nontrivial Γ] {R : Type u_2} (n : ) :
= 1
@[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.to_mv_power_series_symm_apply_coeff {R : Type u_2} [semiring R] {σ : Type u_1} [fintype σ] (f : R) :
theorem hahn_series.coeff_to_mv_power_series {R : Type u_2} [semiring R] {σ : Type u_3} [fintype σ] {f : hahn_series →₀ ) R} {n : σ →₀ } :
= f.coeff n
theorem hahn_series.coeff_to_mv_power_series_symm {R : Type u_2} [semiring R] {σ : Type u_3} [fintype σ] {f : R} {n : σ →₀ } :
= f
@[simp]
theorem hahn_series.to_power_series_alg_apply (R : Type u_2) {A : Type u_3} [semiring A] [ A] (ᾰ : A) :
noncomputable def hahn_series.to_power_series_alg (R : Type u_2) {A : Type u_3} [semiring A] [ A] :

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

Equations
@[simp]
theorem hahn_series.to_power_series_alg_symm_apply (R : Type u_2) {A : Type u_3} [semiring A] [ A] (ᾰ : power_series A) :
noncomputable def hahn_series.of_power_series_alg (Γ : Type u_1) (R : Type u_2) {A : Type u_3} [semiring A] [ A] [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) {A : Type u_3} [semiring A] [ A] [nontrivial Γ] (ᾰ : power_series A) (b : Γ) :
ᾰ).coeff b = dite (∃ (a : ), ¬ a) = 0 a = b) (λ (h : ∃ (a : ), ¬ a) = 0 a = b), (classical.some _)) ᾰ) (λ (h : ¬∃ (a : ), ¬ a) = 0 a = b), 0)
@[protected, instance]
noncomputable def hahn_series.power_series_algebra (Γ : Type u_1) (R : Type u_2) [nontrivial Γ] {S : Type u_3} [ (power_series R)] :
R)
Equations
theorem hahn_series.algebra_map_apply' (Γ : Type u_1) {R : Type u_2} [nontrivial Γ] {S : Type u_4} [ (power_series R)] (x : S) :
R)) x = ( (power_series R)) x)
@[simp]
theorem polynomial.algebra_map_hahn_series_apply (Γ : Type u_1) {R : Type u_2} [nontrivial Γ] (f : polynomial R) :
R)) f =
theorem polynomial.algebra_map_hahn_series_injective (Γ : Type u_1) {R : Type u_2} [nontrivial Γ] :
noncomputable def hahn_series.add_val (Γ : Type u_1) (R : Type u_2) [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} [ring R] [is_domain R] {x : R} :
R) x = ite (x = 0) (x.order)
@[simp]
theorem hahn_series.add_val_apply_of_ne {Γ : Type u_1} {R : Type u_2} [ring R] [is_domain R] {x : R} (hx : x 0) :
R) x = (x.order)
theorem hahn_series.add_val_le_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [ring R] [is_domain R] {x : R} {g : Γ} (h : x.coeff g 0) :
R) x g
theorem hahn_series.is_pwo_Union_support_powers {Γ : Type u_1} {R : Type u_2} [ring R] [is_domain R] {x : R} (hx : 0 < R) x) :
(⋃ (n : ), (x ^ n).support).is_pwo
structure hahn_series.summable_family (Γ : Type u_1) (R : Type u_2) (α : 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} {α : Type u_3} :
(λ (_x : , α → R)
Equations
theorem hahn_series.summable_family.is_pwo_Union_support {Γ : Type u_1} {R : Type u_2} {α : Type u_3} (s : α) :
(⋃ (a : α), (s a).support).is_pwo
theorem hahn_series.summable_family.finite_co_support {Γ : Type u_1} {R : Type u_2} {α : Type u_3} (s : α) (g : Γ) :
(function.support (λ (a : α), (s a).coeff g)).finite
theorem hahn_series.summable_family.coe_injective {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
@[ext]
theorem hahn_series.summable_family.ext {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s t : α} (h : ∀ (a : α), s a = t a) :
s = t
@[protected, instance]
def hahn_series.summable_family.has_add {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
Equations
@[protected, instance]
def hahn_series.summable_family.has_zero {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
Equations
@[protected, instance]
def hahn_series.summable_family.inhabited {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.coe_add {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s t : α} :
(s + t) = s + t
theorem hahn_series.summable_family.add_apply {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s t : α} {a : α} :
(s + t) a = s a + t a
@[simp]
theorem hahn_series.summable_family.coe_zero {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
0 = 0
theorem hahn_series.summable_family.zero_apply {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {a : α} :
0 a = 0
@[protected, instance]
def hahn_series.summable_family.add_comm_monoid {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
Equations
noncomputable def hahn_series.summable_family.hsum {Γ : Type u_1} {R : Type u_2} {α : Type u_3} (s : α) :
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} {α : Type u_3} {s : α} {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} {α : Type u_3} {s : α} :
s.hsum.support ⋃ (a : α), (s a).support
@[simp]
theorem hahn_series.summable_family.hsum_add {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s t : α} :
(s + t).hsum = s.hsum + t.hsum
@[protected, instance]
def hahn_series.summable_family.add_comm_group {Γ : Type u_1} {R : Type u_2} {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.coe_neg {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s : α} :
theorem hahn_series.summable_family.neg_apply {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s : α} {a : α} :
(-s) a = -s a
@[simp]
theorem hahn_series.summable_family.coe_sub {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s t : α} :
(s - t) = s - t
theorem hahn_series.summable_family.sub_apply {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {s t : α} {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} [semiring R] {α : Type u_3} :
has_smul R) α)
Equations
@[simp]
theorem hahn_series.summable_family.smul_apply {Γ : Type u_1} {R : Type u_2} [semiring R] {α : Type u_3} {x : R} {s : α} {a : α} :
(x s) a = x * s a
@[protected, instance]
noncomputable def hahn_series.summable_family.module {Γ : Type u_1} {R : Type u_2} [semiring R] {α : Type u_3} :
module R) α)
Equations
@[simp]
theorem hahn_series.summable_family.hsum_smul {Γ : Type u_1} {R : Type u_2} [semiring R] {α : Type u_3} {x : R} {s : α} :
(x s).hsum = x * s.hsum
@[simp]
theorem hahn_series.summable_family.lsum_apply {Γ : Type u_1} {R : Type u_2} [semiring R] {α : Type u_3} (s : α) :
noncomputable def hahn_series.summable_family.lsum {Γ : Type u_1} {R : Type u_2} [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} {α : Type u_3} {R : Type u_2} [ring R] {s t : α} :
(s - t).hsum = s.hsum - t.hsum
def hahn_series.summable_family.of_finsupp {Γ : Type u_1} {R : Type u_2} {α : Type u_3} (f : α →₀ 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} {α : Type u_3} {f : α →₀ R} :
@[simp]
theorem hahn_series.summable_family.hsum_of_finsupp {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {f : α →₀ R} :
= f.sum (λ (a : α), id)
noncomputable def hahn_series.summable_family.emb_domain {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (s : α) (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} {α : Type u_3} {β : Type u_4} (s : α) (f : α β) {b : β} :
(s.emb_domain f) b = dite (b (λ (h : b , s (classical.some h)) (λ (h : b , 0)
@[simp]
theorem hahn_series.summable_family.emb_domain_image {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (s : α) (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} {α : Type u_3} {β : Type u_4} (s : α) (f : α β) {b : β} (h : b ) :
(s.emb_domain f) b = 0
@[simp]
theorem hahn_series.summable_family.hsum_emb_domain {Γ : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (s : α) (f : α β) :
noncomputable def hahn_series.summable_family.powers {Γ : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] (x : R) (hx : 0 < R) x) :

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

Equations
@[simp]
theorem hahn_series.summable_family.coe_powers {Γ : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {x : R} (hx : 0 < R) x) :
theorem hahn_series.summable_family.emb_domain_succ_smul_powers {Γ : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {x : R} (hx : 0 < R) x) :
theorem hahn_series.summable_family.one_sub_self_mul_hsum_powers {Γ : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {x : R} (hx : 0 < R) x) :
(1 - x) * = 1
theorem hahn_series.unit_aux {Γ : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] (x : R) {r : R} (hr : r * x.coeff x.order = 1) :
0 < R) (1 - * (hahn_series.single (-x.order)) 1 * x)
theorem hahn_series.is_unit_iff {Γ : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {x : R} :
@[protected, instance]
noncomputable def hahn_series.field {Γ : Type u_1} {R : Type u_2} [field R] :
Equations