# Documentation

Mathlib.RingTheory.HahnSeries

# Hahn Series #

If Γ is ordered and R has zero, then HahnSeries Γ 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 HahnSeries Γ R, with the most studied case being when Γ is a linearly ordered abelian group and R is a field, in which case HahnSeries Γ 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 RingTheory/LaurentSeries.

## Main Definitions #

• If Γ is ordered and R has zero, then HahnSeries Γ 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 HahnSeries Γ R.
• If R is a (commutative) (semi-)ring, then so is HahnSeries Γ R.
• HahnSeries.addVal Γ R defines an AddValuation on HahnSeries Γ R when Γ is linearly ordered.
• A HahnSeries.SummableFamily 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, HahnSeries.SummableFamily.hsum, which can be bundled as a LinearMap as HahnSeries.SummableFamily.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 HahnSeries.SummableFamily, and formally summable families whose sums do not converge topologically.
• Laurent series over R are implemented as HahnSeries ℤ R in the file RingTheory/LaurentSeries.

## TODO #

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

## References #

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]
theorem HahnSeries.ext_iff {Γ : Type u_1} {R : Type u_2} :
∀ {inst : } {inst_1 : Zero R} (x y : ), x = y x.coeff = y.coeff
theorem HahnSeries.ext {Γ : Type u_1} {R : Type u_2} :
∀ {inst : } {inst_1 : Zero R} (x y : ), x.coeff = y.coeffx = y
structure HahnSeries (Γ : Type u_1) (R : Type u_2) [] [Zero R] :
Type (max u_1 u_2)

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

Instances For
theorem HahnSeries.coeff_injective {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
Function.Injective HahnSeries.coeff
@[simp]
theorem HahnSeries.coeff_inj {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } {y : } :
x.coeff = y.coeff x = y
def HahnSeries.support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :
Set Γ

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

Instances For
@[simp]
theorem HahnSeries.isPwo_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :
@[simp]
theorem HahnSeries.isWf_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :
@[simp]
theorem HahnSeries.mem_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) (a : Γ) :
0
instance HahnSeries.instZeroHahnSeries {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
Zero ()
instance HahnSeries.instInhabitedHahnSeries {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
instance HahnSeries.instSubsingletonHahnSeries {Γ : Type u_1} {R : Type u_2} [] [Zero R] [] :
@[simp]
theorem HahnSeries.zero_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} :
= 0
@[simp]
theorem HahnSeries.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x.coeff = 0 x = 0
theorem HahnSeries.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } {g : Γ} (h : 0) :
x 0
@[simp]
theorem HahnSeries.support_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
@[simp]
theorem HahnSeries.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x 0
@[simp]
theorem HahnSeries.support_eq_empty_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x = 0
def HahnSeries.single {Γ : Type u_1} {R : Type u_2} [] [Zero R] (a : Γ) :
ZeroHom R ()

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

Instances For
@[simp]
theorem HahnSeries.single_coeff_same {Γ : Type u_1} {R : Type u_2} [] [Zero R] (a : Γ) (r : R) :
HahnSeries.coeff (↑() r) a = r
@[simp]
theorem HahnSeries.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {b : Γ} {r : R} (h : b a) :
HahnSeries.coeff (↑() r) b = 0
theorem HahnSeries.single_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {b : Γ} {r : R} :
HahnSeries.coeff (↑() r) b = if b = a then r else 0
@[simp]
theorem HahnSeries.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} (h : r 0) :
HahnSeries.support (↑() r) = {a}
theorem HahnSeries.support_single_subset {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} :
HahnSeries.support (↑() r) {a}
theorem HahnSeries.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} {b : Γ} (h : b HahnSeries.support (↑() r)) :
b = a
theorem HahnSeries.single_eq_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} :
↑() 0 = 0
theorem HahnSeries.single_injective {Γ : Type u_1} {R : Type u_2} [] [Zero R] (a : Γ) :
theorem HahnSeries.single_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} (h : r 0) :
↑() r 0
@[simp]
theorem HahnSeries.single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} :
↑() r = 0 r = 0
instance HahnSeries.instNontrivialHahnSeries {Γ : Type u_1} {R : Type u_2} [] [Zero R] [] [] :
def HahnSeries.order {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] (x : ) :
Γ

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.

Instances For
@[simp]
theorem HahnSeries.order_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] :
theorem HahnSeries.order_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } (hx : x 0) :
= Set.IsWf.min (_ : ) (_ : )
theorem HahnSeries.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } (hx : x 0) :
theorem HahnSeries.order_le_of_coeff_ne_zero {R : Type u_2} [Zero R] {Γ : Type u_3} {x : } {g : Γ} (h : 0) :
@[simp]
theorem HahnSeries.order_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} [Zero Γ] (h : r 0) :
HahnSeries.order (↑() r) = a
theorem HahnSeries.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } {i : Γ} (hi : ) :
= 0
def HahnSeries.embDomain {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] (f : Γ ↪o Γ') :
HahnSeries Γ' R

Extends the domain of a HahnSeries by an OrderEmbedding.

Instances For
@[simp]
theorem HahnSeries.embDomain_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } {a : Γ} :
HahnSeries.coeff () (f a) =
@[simp]
theorem HahnSeries.embDomain_mk_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : ΓΓ'} (hfi : ) (hf : ∀ (g g' : Γ), f g f g' g g') {x : } {a : Γ} :
HahnSeries.coeff (HahnSeries.embDomain { toEmbedding := { toFun := f, inj' := hfi }, map_rel_iff' := fun {a b} => hf a b } x) (f a) =
theorem HahnSeries.embDomain_notin_image_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } {b : Γ'} (hb : ¬b ) :
= 0
theorem HahnSeries.support_embDomain_subset {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } :
theorem HahnSeries.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } {b : Γ'} (hb : ¬b ) :
= 0
@[simp]
theorem HahnSeries.embDomain_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} :
@[simp]
theorem HahnSeries.embDomain_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {g : Γ} {r : R} :
HahnSeries.embDomain f (↑() r) = ↑(HahnSeries.single (f g)) r
theorem HahnSeries.embDomain_injective {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} :
instance HahnSeries.instAddHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [] [] :
instance HahnSeries.instAddMonoidHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [] [] :
@[simp]
theorem HahnSeries.add_coeff' {Γ : Type u_1} {R : Type u_2} [] [] {x : } {y : } :
(x + y).coeff = x.coeff + y.coeff
theorem HahnSeries.add_coeff {Γ : Type u_1} {R : Type u_2} [] [] {x : } {y : } {a : Γ} :
theorem HahnSeries.support_add_subset {Γ : Type u_1} {R : Type u_2} [] [] {x : } {y : } :
theorem HahnSeries.min_order_le_order_add {R : Type u_2} [] {Γ : Type u_3} {x : } {y : } (hxy : x + y 0) :
@[simp]
theorem HahnSeries.single.addMonoidHom_apply {Γ : Type u_1} {R : Type u_2} [] [] (a : Γ) :
∀ (a : R),
def HahnSeries.single.addMonoidHom {Γ : Type u_1} {R : Type u_2} [] [] (a : Γ) :
R →+

single as an additive monoid/group homomorphism

Instances For
@[simp]
theorem HahnSeries.coeff.addMonoidHom_apply {Γ : Type u_1} {R : Type u_2} [] [] (g : Γ) (f : ) :
def HahnSeries.coeff.addMonoidHom {Γ : Type u_1} {R : Type u_2} [] [] (g : Γ) :
→+ R

coeff g as an additive monoid/group homomorphism

Instances For
theorem HahnSeries.embDomain_add {Γ : Type u_1} {R : Type u_2} [] [] {Γ' : Type u_3} [] (f : Γ ↪o Γ') (x : ) (y : ) :
@[simp]
theorem HahnSeries.neg_coeff' {Γ : Type u_1} {R : Type u_2} [] [] {x : } :
(-x).coeff = -x.coeff
theorem HahnSeries.neg_coeff {Γ : Type u_1} {R : Type u_2} [] [] {x : } {a : Γ} :
=
@[simp]
theorem HahnSeries.support_neg {Γ : Type u_1} {R : Type u_2} [] [] {x : } :
@[simp]
theorem HahnSeries.sub_coeff' {Γ : Type u_1} {R : Type u_2} [] [] {x : } {y : } :
(x - y).coeff = x.coeff - y.coeff
theorem HahnSeries.sub_coeff {Γ : Type u_1} {R : Type u_2} [] [] {x : } {y : } {a : Γ} :
@[simp]
theorem HahnSeries.order_neg {Γ : Type u_1} {R : Type u_2} [] [] [Zero Γ] {f : } :
instance HahnSeries.instSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [] {V : Type u_3} [] [] [] :
SMul R ()
@[simp]
theorem HahnSeries.smul_coeff {Γ : Type u_1} {R : Type u_2} [] {V : Type u_3} [] [] [] {r : R} {x : } {a : Γ} :
instance HahnSeries.instIsScalarTowerHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [] {V : Type u_3} [] [] [] {S : Type u_4} [] [] [SMul R S] [] :
@[simp]
theorem HahnSeries.single.linearMap_apply {Γ : Type u_1} {R : Type u_2} [] [] (a : Γ) :
∀ (a : R),
def HahnSeries.single.linearMap {Γ : Type u_1} {R : Type u_2} [] [] (a : Γ) :

single as a linear map

Instances For
@[simp]
theorem HahnSeries.coeff.linearMap_apply {Γ : Type u_1} {R : Type u_2} [] [] (g : Γ) :
∀ (a : ),
def HahnSeries.coeff.linearMap {Γ : Type u_1} {R : Type u_2} [] [] (g : Γ) :

coeff g as a linear map

Instances For
theorem HahnSeries.embDomain_smul {Γ : Type u_1} {R : Type u_2} [] [] {Γ' : Type u_4} [] (f : Γ ↪o Γ') (r : R) (x : ) :
@[simp]
theorem HahnSeries.embDomainLinearMap_apply {Γ : Type u_1} {R : Type u_2} [] [] {Γ' : Type u_4} [] (f : Γ ↪o Γ') :
∀ (a : ),
def HahnSeries.embDomainLinearMap {Γ : Type u_1} {R : Type u_2} [] [] {Γ' : Type u_4} [] (f : Γ ↪o Γ') :

Extending the domain of Hahn series is a linear map.

Instances For
instance HahnSeries.instOneHahnSeriesToPartialOrder {Γ : Type u_1} {R : Type u_2} [Zero R] [One R] :
One ()
@[simp]
theorem HahnSeries.one_coeff {Γ : Type u_1} {R : Type u_2} [Zero R] [One R] {a : Γ} :
= if a = 0 then 1 else 0
@[simp]
theorem HahnSeries.single_zero_one {R : Type u_2} [Zero R] [One R] :
↑() 1 = 1
@[simp]
theorem HahnSeries.support_one {Γ : Type u_1} {R : Type u_2} [] [] :
= {0}
@[simp]
theorem HahnSeries.order_one {Γ : Type u_1} {R : Type u_2} [] :
theorem HahnSeries.mul_coeff {Γ : Type u_1} {R : Type u_2} {x : } {y : } {a : Γ} :
HahnSeries.coeff (x * y) a = Finset.sum (Finset.addAntidiagonal (_ : ) (_ : ) a) fun ij => HahnSeries.coeff x ij.fst * HahnSeries.coeff y ij.snd
theorem HahnSeries.mul_coeff_right' {Γ : Type u_1} {R : Type u_2} {x : } {y : } {a : Γ} {s : Set Γ} (hs : ) (hys : ) :
HahnSeries.coeff (x * y) a = Finset.sum (Finset.addAntidiagonal (_ : ) hs a) fun ij => HahnSeries.coeff x ij.fst * HahnSeries.coeff y ij.snd
theorem HahnSeries.mul_coeff_left' {Γ : Type u_1} {R : Type u_2} {x : } {y : } {a : Γ} {s : Set Γ} (hs : ) (hxs : ) :
HahnSeries.coeff (x * y) a = Finset.sum (Finset.addAntidiagonal hs (_ : ) a) fun ij => HahnSeries.coeff x ij.fst * HahnSeries.coeff y ij.snd
theorem HahnSeries.single_mul_coeff_add {Γ : Type u_1} {R : Type u_2} {r : R} {x : } {a : Γ} {b : Γ} :
HahnSeries.coeff (↑() r * x) (a + b) = r *
theorem HahnSeries.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} {r : R} {x : } {a : Γ} {b : Γ} :
HahnSeries.coeff (x * ↑() r) (a + b) = * r
@[simp]
theorem HahnSeries.mul_single_zero_coeff {Γ : Type u_1} {R : Type u_2} {r : R} {x : } {a : Γ} :
HahnSeries.coeff (x * ↑() r) a = * r
theorem HahnSeries.single_zero_mul_coeff {Γ : Type u_1} {R : Type u_2} {r : R} {x : } {a : Γ} :
HahnSeries.coeff (↑() r * x) a = r *
@[simp]
theorem HahnSeries.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [] {r : R} {x : } :
↑() r * x = r x
theorem HahnSeries.support_mul_subset_add_support {Γ : Type u_1} {R : Type u_2} {x : } {y : } :
theorem HahnSeries.mul_coeff_order_add_order {R : Type u_2} {Γ : Type u_3} (x : ) (y : ) :
HahnSeries.coeff (x * y) () =
@[simp]
theorem HahnSeries.order_mul {R : Type u_2} {Γ : Type u_3} [] {x : } {y : } (hx : x 0) (hy : y 0) :
@[simp]
theorem HahnSeries.order_pow {R : Type u_2} {Γ : Type u_3} [] [] (x : ) (n : ) :
@[simp]
theorem HahnSeries.single_mul_single {Γ : Type u_1} {R : Type u_2} {a : Γ} {b : Γ} {r : R} {s : R} :
↑() r * ↑() s = ↑(HahnSeries.single (a + b)) (r * s)
@[simp]
theorem HahnSeries.C_apply {Γ : Type u_1} {R : Type u_2} [] (a : R) :
HahnSeries.C a = ↑() a
def HahnSeries.C {Γ : Type u_1} {R : Type u_2} [] :

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

Instances For
theorem HahnSeries.C_zero {Γ : Type u_1} {R : Type u_2} [] :
HahnSeries.C 0 = 0
theorem HahnSeries.C_one {Γ : Type u_1} {R : Type u_2} [] :
HahnSeries.C 1 = 1
theorem HahnSeries.C_injective {Γ : Type u_1} {R : Type u_2} [] :
Function.Injective HahnSeries.C
theorem HahnSeries.C_ne_zero {Γ : Type u_1} {R : Type u_2} [] {r : R} (h : r 0) :
HahnSeries.C r 0
theorem HahnSeries.order_C {Γ : Type u_1} {R : Type u_2} [] {r : R} :
HahnSeries.order (HahnSeries.C r) = 0
theorem HahnSeries.C_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [] {r : R} {x : } :
HahnSeries.C r * x = r x
theorem HahnSeries.embDomain_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 : ) :
theorem HahnSeries.embDomain_one {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} [] (f : Γ ↪o Γ') (hf : f 0 = 0) :
@[simp]
theorem HahnSeries.embDomainRingHom_apply {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} [] (f : Γ →+ Γ') (hfi : ) (hf : ∀ (g g' : Γ), f g f g' g g') :
∀ (a : ), ↑() a = HahnSeries.embDomain { toEmbedding := { toFun := f, inj' := hfi }, map_rel_iff' := fun {a b} => hf a b } a
def HahnSeries.embDomainRingHom {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} [] (f : Γ →+ Γ') (hfi : ) (hf : ∀ (g g' : Γ), f g f g' g g') :

Extending the domain of Hahn series is a ring homomorphism.

Instances For
theorem HahnSeries.embDomainRingHom_C {Γ : Type u_1} {R : Type u_2} {Γ' : Type u_3} [] {f : Γ →+ Γ'} {hfi : } {hf : ∀ (g g' : Γ), f g f g' g g'} {r : R} :
↑() (HahnSeries.C r) = HahnSeries.C r
theorem HahnSeries.C_eq_algebraMap {Γ : Type u_1} {R : Type u_2} [] :
HahnSeries.C = algebraMap R ()
theorem HahnSeries.algebraMap_apply {Γ : Type u_1} {R : Type u_2} [] {A : Type u_3} [] [Algebra R A] {r : R} :
↑(algebraMap R ()) r = HahnSeries.C (↑() r)
@[simp]
theorem HahnSeries.embDomainAlgHom_apply_coeff {Γ : Type u_1} {R : Type u_2} [] {A : Type u_3} [] [Algebra R A] {Γ' : Type u_4} (f : Γ →+ Γ') (hfi : ) (hf : ∀ (g g' : Γ), f g f g' g g') :
∀ (a : ) (b : Γ'), HahnSeries.coeff (↑() a) b = if h : x, ¬ = 0 f x = b then HahnSeries.coeff a (Classical.choose (_ : x, (fun x => ¬ = 0 f x = b) x)) else 0
def HahnSeries.embDomainAlgHom {Γ : Type u_1} {R : Type u_2} [] {A : Type u_3} [] [Algebra R A] {Γ' : Type u_4} (f : Γ →+ Γ') (hfi : ) (hf : ∀ (g g' : Γ), f g f g' g g') :

Extending the domain of Hahn series is an algebra homomorphism.

Instances For
@[simp]
theorem HahnSeries.toPowerSeries_apply {R : Type u_2} [] (f : ) :
HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff
@[simp]
theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [] (f : ) (n : ) :
HahnSeries.coeff (↑(RingEquiv.symm HahnSeries.toPowerSeries) f) n = ↑() f
def HahnSeries.toPowerSeries {R : Type u_2} [] :

The ring HahnSeries ℕ R is isomorphic to PowerSeries R.

Instances For
theorem HahnSeries.coeff_toPowerSeries {R : Type u_2} [] {f : } {n : } :
↑() (HahnSeries.toPowerSeries f) =
theorem HahnSeries.coeff_toPowerSeries_symm {R : Type u_2} [] {f : } {n : } :
HahnSeries.coeff (↑(RingEquiv.symm HahnSeries.toPowerSeries) f) n = ↑() f
def HahnSeries.ofPowerSeries (Γ : Type u_1) (R : Type u_2) [] :

Casts a power series as a Hahn series with coefficients from a StrictOrderedSemiring.

Instances For
theorem HahnSeries.ofPowerSeries_injective {Γ : Type u_1} {R : Type u_2} [] :
theorem HahnSeries.ofPowerSeries_apply {Γ : Type u_1} {R : Type u_2} [] (x : ) :
↑() x = HahnSeries.embDomain { toEmbedding := { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) }, map_rel_iff' := (_ : ∀ {a b : }, { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } a { toFun := Nat.cast, inj' := (_ : Function.Injective Nat.cast) } b a b) } (↑(RingEquiv.symm HahnSeries.toPowerSeries) x)
theorem HahnSeries.ofPowerSeries_apply_coeff {Γ : Type u_1} {R : Type u_2} [] (x : ) (n : ) :
HahnSeries.coeff (↑() x) n = ↑() x
@[simp]
theorem HahnSeries.ofPowerSeries_C {Γ : Type u_1} {R : Type u_2} [] (r : R) :
↑() (↑() r) = HahnSeries.C r
@[simp]
theorem HahnSeries.ofPowerSeries_X {Γ : Type u_1} {R : Type u_2} [] :
↑() PowerSeries.X = ↑() 1
@[simp]
theorem HahnSeries.ofPowerSeries_X_pow {Γ : Type u_1} {R : Type u_3} [] (n : ) :
↑() (PowerSeries.X ^ n) = ↑() 1
@[simp]
theorem HahnSeries.toMvPowerSeries_symm_apply_coeff {R : Type u_2} [] {σ : Type u_3} [] (f : ) :
(↑(RingEquiv.symm HahnSeries.toMvPowerSeries) f).coeff = f
@[simp]
theorem HahnSeries.toMvPowerSeries_apply {R : Type u_2} [] {σ : Type u_3} [] (f : HahnSeries (σ →₀ ) R) :
∀ (a : σ →₀ ), HahnSeries.toMvPowerSeries f a =
def HahnSeries.toMvPowerSeries {R : Type u_2} [] {σ : Type u_3} [] :

The ring HahnSeries (σ →₀ ℕ) R is isomorphic to MvPowerSeries σ 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 MvPowerSeries. After importing Algebra.Order.Pi the ring HahnSeries (σ → ℕ) R could be constructed instead.

Instances For
theorem HahnSeries.coeff_toMvPowerSeries {R : Type u_2} [] {σ : Type u_3} [] {f : HahnSeries (σ →₀ ) R} {n : σ →₀ } :
↑() (HahnSeries.toMvPowerSeries f) =
theorem HahnSeries.coeff_toMvPowerSeries_symm {R : Type u_2} [] {σ : Type u_3} [] {f : } {n : σ →₀ } :
HahnSeries.coeff (↑(RingEquiv.symm HahnSeries.toMvPowerSeries) f) n = ↑() f
@[simp]
theorem HahnSeries.toPowerSeriesAlg_symm_apply_coeff (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] (f : ) (n : ) :
= ↑() f
@[simp]
theorem HahnSeries.toPowerSeriesAlg_apply (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] (f : ) :
= PowerSeries.mk f.coeff
def HahnSeries.toPowerSeriesAlg (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] :

The R-algebra HahnSeries ℕ A is isomorphic to PowerSeries A.

Instances For
@[simp]
theorem HahnSeries.ofPowerSeriesAlg_apply_coeff (Γ : Type u_1) (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] :
∀ (a : ) (b : Γ), HahnSeries.coeff (↑() a) b = if h : x, ¬↑() a = 0 x = b then ↑(PowerSeries.coeff A (Classical.choose (_ : x, (fun x => ¬↑() a = 0 x = b) x))) a else 0
def HahnSeries.ofPowerSeriesAlg (Γ : Type u_1) (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] :

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

Instances For
instance HahnSeries.powerSeriesAlgebra (Γ : Type u_1) (R : Type u_2) [] {S : Type u_4} [] [Algebra S ()] :
Algebra S ()
theorem HahnSeries.algebraMap_apply' (Γ : Type u_1) {R : Type u_2} [] {S : Type u_4} [] [Algebra S ()] (x : S) :
↑(algebraMap S ()) x = ↑() (↑() x)
@[simp]
theorem Polynomial.algebraMap_hahnSeries_apply (Γ : Type u_1) {R : Type u_2} [] (f : ) :
↑(algebraMap () ()) f = ↑() f
def HahnSeries.addVal (Γ : Type u_1) (R : Type u_2) [Ring R] [] :

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

Instances For
theorem HahnSeries.addVal_apply {Γ : Type u_1} {R : Type u_2} [Ring R] [] {x : } :
↑() x = if x = 0 then else ↑()
@[simp]
theorem HahnSeries.addVal_apply_of_ne {Γ : Type u_1} {R : Type u_2} [Ring R] [] {x : } (hx : x 0) :
↑() x = ↑()
theorem HahnSeries.addVal_le_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [Ring R] [] {x : } {g : Γ} (h : 0) :
↑() x g
theorem HahnSeries.isPwo_iUnion_support_powers {Γ : Type u_1} {R : Type u_2} [Ring R] [] {x : } (hx : 0 < ↑() x) :
Set.IsPwo (⋃ (n : ), HahnSeries.support (x ^ n))
structure HahnSeries.SummableFamily (Γ : Type u_1) (R : Type u_2) [] [] (α : Type u_3) :
Type (max (max u_1 u_2) u_3)
• toFun : α
• isPwo_iUnion_support' : Set.IsPwo (⋃ (a : α), )
• finite_co_support' : ∀ (g : Γ), Set.Finite {a | }

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
theorem HahnSeries.SummableFamily.isPwo_iUnion_support {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} (s : ) :
Set.IsPwo (⋃ (a : α), HahnSeries.support (s a))
theorem HahnSeries.SummableFamily.finite_co_support {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} (s : ) (g : Γ) :
theorem HahnSeries.SummableFamily.coe_injective {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} :
Function.Injective FunLike.coe
theorem HahnSeries.SummableFamily.ext {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {t : } (h : ∀ (a : α), s a = t a) :
s = t
instance HahnSeries.SummableFamily.instAddSummableFamily {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} :
instance HahnSeries.SummableFamily.instZeroSummableFamily {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} :
Zero ()
instance HahnSeries.SummableFamily.instInhabitedSummableFamily {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} :
@[simp]
theorem HahnSeries.SummableFamily.coe_add {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {t : } :
↑(s + t) = s + t
theorem HahnSeries.SummableFamily.add_apply {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {t : } {a : α} :
↑(s + t) a = s a + t a
@[simp]
theorem HahnSeries.SummableFamily.coe_zero {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} :
0 = 0
theorem HahnSeries.SummableFamily.zero_apply {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {a : α} :
0 a = 0
instance HahnSeries.SummableFamily.instAddCommMonoidSummableFamily {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} :
def HahnSeries.SummableFamily.hsum {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} (s : ) :

The infinite sum of a SummableFamily of Hahn series.

Instances For
@[simp]
theorem HahnSeries.SummableFamily.hsum_coeff {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {g : Γ} :
= ∑ᶠ (i : α), HahnSeries.coeff (s i) g
theorem HahnSeries.SummableFamily.support_hsum_subset {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } :
⋃ (a : α), HahnSeries.support (s a)
@[simp]
theorem HahnSeries.SummableFamily.hsum_add {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {t : } :
@[simp]
theorem HahnSeries.SummableFamily.coe_neg {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } :
↑(-s) = -s
theorem HahnSeries.SummableFamily.neg_apply {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {a : α} :
↑(-s) a = -s a
@[simp]
theorem HahnSeries.SummableFamily.coe_sub {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {t : } :
↑(s - t) = s - t
theorem HahnSeries.SummableFamily.sub_apply {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {s : } {t : } {a : α} :
↑(s - t) a = s a - t a
@[simp]
theorem HahnSeries.SummableFamily.smul_apply {Γ : Type u_1} {R : Type u_2} [] {α : Type u_3} {x : } {s : } {a : α} :
↑(x s) a = x * s a
@[simp]
theorem HahnSeries.SummableFamily.hsum_smul {Γ : Type u_1} {R : Type u_2} [] {α : Type u_3} {x : } {s : } :
@[simp]
theorem HahnSeries.SummableFamily.lsum_apply {Γ : Type u_1} {R : Type u_2} [] {α : Type u_3} (s : ) :
HahnSeries.SummableFamily.lsum s =
def HahnSeries.SummableFamily.lsum {Γ : Type u_1} {R : Type u_2} [] {α : Type u_3} :

The summation of a summable_family as a LinearMap.

Instances For
@[simp]
theorem HahnSeries.SummableFamily.hsum_sub {Γ : Type u_1} {α : Type u_3} {R : Type u_4} [Ring R] {s : } {t : } :
def HahnSeries.SummableFamily.ofFinsupp {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} (f : α →₀ ) :

A family with only finitely many nonzero elements is summable.

Instances For
@[simp]
theorem HahnSeries.SummableFamily.coe_ofFinsupp {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {f : α →₀ } :
@[simp]
theorem HahnSeries.SummableFamily.hsum_ofFinsupp {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {f : α →₀ } :
def HahnSeries.SummableFamily.embDomain {Γ : 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.

Instances For
theorem HahnSeries.SummableFamily.embDomain_apply {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {β : Type u_4} (s : ) (f : α β) {b : β} :
= if h : b then s () else 0
@[simp]
theorem HahnSeries.SummableFamily.embDomain_image {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {β : Type u_4} (s : ) (f : α β) {a : α} :
↑() (f a) = s a
@[simp]
theorem HahnSeries.SummableFamily.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {β : Type u_4} (s : ) (f : α β) {b : β} (h : ¬b ) :
= 0
@[simp]
theorem HahnSeries.SummableFamily.hsum_embDomain {Γ : Type u_1} {R : Type u_2} [] [] {α : Type u_3} {β : Type u_4} (s : ) (f : α β) :
def HahnSeries.SummableFamily.powers {Γ : Type u_1} {R : Type u_2} [] [] (x : ) (hx : 0 < ↑() x) :

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

Instances For
@[simp]
theorem HahnSeries.SummableFamily.coe_powers {Γ : Type u_1} {R : Type u_2} [] [] {x : } (hx : 0 < ↑() x) :
theorem HahnSeries.SummableFamily.embDomain_succ_smul_powers {Γ : Type u_1} {R : Type u_2} [] [] {x : } (hx : 0 < ↑() x) :
theorem HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers {Γ : Type u_1} {R : Type u_2} [] [] {x : } (hx : 0 < ↑() x) :
= 1
theorem HahnSeries.unit_aux {Γ : Type u_1} {R : Type u_2} [] [] (x : ) {r : R} (hr : = 1) :
0 < ↑() (1 - HahnSeries.C r * ↑() 1 * x)
theorem HahnSeries.isUnit_iff {Γ : Type u_1} {R : Type u_2} [] [] {x : } :