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 : PartialOrder Γ} {inst_1 : Zero R} (x y : HahnSeries Γ R), x = y ↔ x.coeff = y.coeff

theorem HahnSeries.ext {Γ : Type u_1} {R : Type u_2} : ∀ {inst : PartialOrder Γ} {inst_1 : Zero R} (x y : HahnSeries Γ R), x.coeff = y.coeff → x = y

structure HahnSeries (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [Zero R] : Type (max u_1 u_2)

• coeff : Γ → R
• isPwo_support' : Set.IsPwo (Function.support s.coeff)

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.

theorem HahnSeries.coeff_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] : Function.Injective HahnSeries.coeff

@[simp]

theorem HahnSeries.coeff_inj {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : x.coeff = y.coeff ↔ x = y

def HahnSeries.support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) : Set Γ

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

Equations

• HahnSeries.support x = Function.support x.coeff

@[simp]

theorem HahnSeries.isPwo_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) : Set.IsPwo (HahnSeries.support x)

@[simp]

theorem HahnSeries.isWf_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) : Set.IsWf (HahnSeries.support x)

@[simp]

theorem HahnSeries.mem_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) (a : Γ) : a ∈ HahnSeries.support x ↔ HahnSeries.coeff x a ≠ 0

instance HahnSeries.instZeroHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] : Zero (HahnSeries Γ R)

Equations

• HahnSeries.instZeroHahnSeries = { zero := { coeff := 0, isPwo_support' := (_ : Set.IsPwo (Function.support 0)) } }

instance HahnSeries.instInhabitedHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] : Inhabited (HahnSeries Γ R)

Equations

• HahnSeries.instInhabitedHahnSeries = { default := 0 }

instance HahnSeries.instSubsingletonHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Subsingleton R] : Subsingleton (HahnSeries Γ R)

Equations

• @HahnSeries.instSubsingletonHahnSeries = @HahnSeries.instSubsingletonHahnSeries.proof_1

@[simp]

theorem HahnSeries.zero_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} : HahnSeries.coeff 0 a = 0

@[simp]

theorem HahnSeries.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} : x.coeff = 0 ↔ x = 0

theorem HahnSeries.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (h : HahnSeries.coeff x g ≠ 0) : x ≠ 0

@[simp]

theorem HahnSeries.support_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] : HahnSeries.support 0 = ∅

@[simp]

theorem HahnSeries.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} : Set.Nonempty (HahnSeries.support x) ↔ x ≠ 0

@[simp]

theorem HahnSeries.support_eq_empty_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} : HahnSeries.support x = ∅ ↔ x = 0

def HahnSeries.single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) : ZeroHom R (HahnSeries Γ R)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.single_coeff_same {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) (r : R) : HahnSeries.coeff (↑(HahnSeries.single a) r) a = r

@[simp]

theorem HahnSeries.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} (h : b ≠ a) : HahnSeries.coeff (↑(HahnSeries.single a) r) b = 0

theorem HahnSeries.single_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} : HahnSeries.coeff (↑(HahnSeries.single a) r) b = if b = a then r else 0

@[simp]

theorem HahnSeries.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) : HahnSeries.support (↑(HahnSeries.single a) r) = {a}

theorem HahnSeries.support_single_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} : HahnSeries.support (↑(HahnSeries.single a) r) ⊆ {a}

theorem HahnSeries.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} {b : Γ} (h : b ∈ HahnSeries.support (↑(HahnSeries.single a) r)) : b = a

theorem HahnSeries.single_eq_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} : ↑(HahnSeries.single a) 0 = 0

theorem HahnSeries.single_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] (a : Γ) : Function.Injective ↑(HahnSeries.single a)

theorem HahnSeries.single_ne_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) : ↑(HahnSeries.single a) r ≠ 0

@[simp]

theorem HahnSeries.single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} : ↑(HahnSeries.single a) r = 0 ↔ r = 0

instance HahnSeries.instNontrivialHahnSeries {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Nonempty Γ] [Nontrivial R] : Nontrivial (HahnSeries Γ R)

Equations

• @HahnSeries.instNontrivialHahnSeries = @HahnSeries.instNontrivialHahnSeries.proof_1

def HahnSeries.order {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] (x : HahnSeries Γ 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

• HahnSeries.order x = if h : x = 0 then 0 else Set.IsWf.min (_ : Set.IsWf (HahnSeries.support x)) (_ : Set.Nonempty (HahnSeries.support x))

@[simp]

theorem HahnSeries.order_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] : HahnSeries.order 0 = 0

theorem HahnSeries.order_of_ne {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) : HahnSeries.order x = Set.IsWf.min (_ : Set.IsWf (HahnSeries.support x)) (_ : Set.Nonempty (HahnSeries.support x))

theorem HahnSeries.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) : HahnSeries.coeff x (HahnSeries.order x) ≠ 0

theorem HahnSeries.order_le_of_coeff_ne_zero {R : Type u_2} [Zero R] {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] {x : HahnSeries Γ R} {g : Γ} (h : HahnSeries.coeff x g ≠ 0) : HahnSeries.order x ≤ g

@[simp]

theorem HahnSeries.order_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} [Zero Γ] (h : r ≠ 0) : HahnSeries.order (↑(HahnSeries.single a) r) = a

theorem HahnSeries.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} {i : Γ} (hi : i < HahnSeries.order x) : HahnSeries.coeff x i = 0

def HahnSeries.embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] (f : Γ ↪o Γ') : HahnSeries Γ R → HahnSeries Γ' R

Extends the domain of a HahnSeries by an OrderEmbedding.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.embDomain_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (HahnSeries.embDomain f x) (↑f a) = HahnSeries.coeff x a

@[simp]

theorem HahnSeries.embDomain_mk_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ → Γ'} (hfi : Function.Injective f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') {x : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (HahnSeries.embDomain { toEmbedding := { toFun := f, inj' := hfi }, map_rel_iff' := (_ : ∀ {a b : Γ}, f a ≤ f b ↔ a ≤ b) } x) (f a) = HahnSeries.coeff x a

theorem HahnSeries.embDomain_notin_image_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : ¬b ∈ ↑f '' HahnSeries.support x) : HahnSeries.coeff (HahnSeries.embDomain f x) b = 0

theorem HahnSeries.support_embDomain_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} : HahnSeries.support (HahnSeries.embDomain f x) ⊆ ↑f '' HahnSeries.support x

theorem HahnSeries.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : ¬b ∈ Set.range ↑f) : HahnSeries.coeff (HahnSeries.embDomain f x) b = 0

@[simp]

theorem HahnSeries.embDomain_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} : HahnSeries.embDomain f 0 = 0

@[simp]

theorem HahnSeries.embDomain_single {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} {g : Γ} {r : R} : HahnSeries.embDomain f (↑(HahnSeries.single g) r) = ↑(HahnSeries.single (↑f g)) r

theorem HahnSeries.embDomain_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {Γ' : Type u_3} [PartialOrder Γ'] {f : Γ ↪o Γ'} : Function.Injective (HahnSeries.embDomain f)

instance HahnSeries.instAddHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] : Add (HahnSeries Γ R)

Equations

• HahnSeries.instAddHahnSeriesToZero = { add := fun x y => { coeff := x.coeff + y.coeff, isPwo_support' := (_ : Set.IsPwo (Function.support (x.coeff + y.coeff))) } }

instance HahnSeries.instAddMonoidHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] : AddMonoid (HahnSeries Γ R)

Equations

• HahnSeries.instAddMonoidHahnSeriesToZero = AddMonoid.mk (_ : ∀ (x : HahnSeries Γ R), 0 + x = x) (_ : ∀ (x : HahnSeries Γ R), x + 0 = x) nsmulRec

@[simp]

theorem HahnSeries.add_coeff' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : (x + y).coeff = x.coeff + y.coeff

theorem HahnSeries.add_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (x + y) a = HahnSeries.coeff x a + HahnSeries.coeff y a

theorem HahnSeries.support_add_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : HahnSeries.support (x + y) ⊆ HahnSeries.support x ∪ HahnSeries.support y

theorem HahnSeries.min_order_le_order_add {R : Type u_2} [AddMonoid R] {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] {x : HahnSeries Γ R} {y : HahnSeries Γ R} (hxy : x + y ≠ 0) : min (HahnSeries.order x) (HahnSeries.order y) ≤ HahnSeries.order (x + y)

@[simp]

theorem HahnSeries.single.addMonoidHom_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (a : Γ) : ∀ (a_1 : R), ↑(HahnSeries.single.addMonoidHom a) a_1 = ZeroHom.toFun (HahnSeries.single a) a_1

def HahnSeries.single.addMonoidHom {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (a : Γ) : R →+ HahnSeries Γ R

single as an additive monoid/group homomorphism

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.coeff.addMonoidHom_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (g : Γ) (f : HahnSeries Γ R) : ↑(HahnSeries.coeff.addMonoidHom g) f = HahnSeries.coeff f g

def HahnSeries.coeff.addMonoidHom {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (g : Γ) : HahnSeries Γ R →+ R

coeff g as an additive monoid/group homomorphism

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.embDomain_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] {Γ' : Type u_3} [PartialOrder Γ'] (f : Γ ↪o Γ') (x : HahnSeries Γ R) (y : HahnSeries Γ R) : HahnSeries.embDomain f (x + y) = HahnSeries.embDomain f x + HahnSeries.embDomain f y

instance HahnSeries.instAddCommMonoidHahnSeriesToZeroToAddMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] : AddCommMonoid (HahnSeries Γ R)

Equations

• HahnSeries.instAddCommMonoidHahnSeriesToZeroToAddMonoid = let src := inferInstanceAs (AddMonoid (HahnSeries Γ R)); AddCommMonoid.mk (_ : ∀ (x y : HahnSeries Γ R), x + y = y + x)

instance HahnSeries.instAddGroupHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] : AddGroup (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.neg_coeff' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} : (-x).coeff = -x.coeff

theorem HahnSeries.neg_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (-x) a = -HahnSeries.coeff x a

@[simp]

theorem HahnSeries.support_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} : HahnSeries.support (-x) = HahnSeries.support x

@[simp]

theorem HahnSeries.sub_coeff' {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : (x - y).coeff = x.coeff - y.coeff

theorem HahnSeries.sub_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (x - y) a = HahnSeries.coeff x a - HahnSeries.coeff y a

@[simp]

theorem HahnSeries.order_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] [Zero Γ] {f : HahnSeries Γ R} : HahnSeries.order (-f) = HahnSeries.order f

instance HahnSeries.instAddCommGroupHahnSeriesToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] : AddCommGroup (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] : SMul R (HahnSeries Γ V)

Equations

• HahnSeries.instSMulHahnSeriesToZero = { smul := fun r x => { coeff := r • x.coeff, isPwo_support' := (_ : Set.IsPwo (Function.support (r • x.coeff))) } }

@[simp]

theorem HahnSeries.smul_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {r : R} {x : HahnSeries Γ V} {a : Γ} : HahnSeries.coeff (r • x) a = r • HahnSeries.coeff x a

instance HahnSeries.instDistribMulActionHahnSeriesToZeroInstAddMonoidHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] : DistribMulAction R (HahnSeries Γ V)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instIsScalarTowerHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {S : Type u_4} [Monoid S] [DistribMulAction S V] [SMul R S] [IsScalarTower R S V] : IsScalarTower R S (HahnSeries Γ V)

Equations

• @HahnSeries.instIsScalarTowerHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero = @HahnSeries.instIsScalarTowerHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero.proof_1

instance HahnSeries.instSMulCommClassHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {S : Type u_4} [Monoid S] [DistribMulAction S V] [SMulCommClass R S V] : SMulCommClass R S (HahnSeries Γ V)

Equations

• @HahnSeries.instSMulCommClassHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero = @HahnSeries.instSMulCommClassHahnSeriesToZeroInstSMulHahnSeriesToZeroInstSMulHahnSeriesToZero.proof_1

instance HahnSeries.instModuleHahnSeriesToZeroToAddMonoidInstAddCommMonoidHahnSeriesToZeroToAddMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] : Module R (HahnSeries Γ V)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.single.linearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] (a : Γ) : ∀ (a_1 : R), ↑(HahnSeries.single.linearMap a) a_1 = ZeroHom.toFun (↑(HahnSeries.single.addMonoidHom a)) a_1

def HahnSeries.single.linearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] (a : Γ) : R →ₗ[R] HahnSeries Γ R

single as a linear map

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.coeff.linearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] (g : Γ) : ∀ (a : HahnSeries Γ R), ↑(HahnSeries.coeff.linearMap g) a = ZeroHom.toFun (↑(HahnSeries.coeff.addMonoidHom g)) a

def HahnSeries.coeff.linearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] (g : Γ) : HahnSeries Γ R →ₗ[R] R

coeff g as a linear map

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.embDomain_smul {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {Γ' : Type u_4} [PartialOrder Γ'] (f : Γ ↪o Γ') (r : R) (x : HahnSeries Γ R) : HahnSeries.embDomain f (r • x) = r • HahnSeries.embDomain f x

@[simp]

theorem HahnSeries.embDomainLinearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {Γ' : Type u_4} [PartialOrder Γ'] (f : Γ ↪o Γ') : ∀ (a : HahnSeries Γ R), ↑(HahnSeries.embDomainLinearMap f) a = HahnSeries.embDomain f a

def HahnSeries.embDomainLinearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {Γ' : Type u_4} [PartialOrder Γ'] (f : Γ ↪o Γ') : HahnSeries Γ R →ₗ[R] HahnSeries Γ' R

Extending the domain of Hahn series is a linear map.

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instOneHahnSeriesToPartialOrder {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Zero R] [One R] : One (HahnSeries Γ R)

Equations

• HahnSeries.instOneHahnSeriesToPartialOrder = { one := ↑(HahnSeries.single 0) 1 }

@[simp]

theorem HahnSeries.one_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Zero R] [One R] {a : Γ} : HahnSeries.coeff 1 a = if a = 0 then 1 else 0

@[simp]

theorem HahnSeries.single_zero_one {R : Type u_2} [Zero R] [One R] : ↑(HahnSeries.single 0) 1 = 1

@[simp]

theorem HahnSeries.support_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [MulZeroOneClass R] [Nontrivial R] : HahnSeries.support 1 = {0}

@[simp]

theorem HahnSeries.order_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [MulZeroOneClass R] : HahnSeries.order 1 = 0

instance HahnSeries.instMulHahnSeriesToPartialOrderToZeroToMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] : Mul (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.mul_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (x * y) a = Finset.sum (Finset.addAntidiagonal (_ : Set.IsPwo (HahnSeries.support x)) (_ : Set.IsPwo (HahnSeries.support y)) a) fun ij => HahnSeries.coeff x ij.1 * HahnSeries.coeff y ij.2

theorem HahnSeries.mul_coeff_right' {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : Set.IsPwo s) (hys : HahnSeries.support y ⊆ s) : HahnSeries.coeff (x * y) a = Finset.sum (Finset.addAntidiagonal (_ : Set.IsPwo (HahnSeries.support x)) hs a) fun ij => HahnSeries.coeff x ij.1 * HahnSeries.coeff y ij.2

theorem HahnSeries.mul_coeff_left' {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : Set.IsPwo s) (hxs : HahnSeries.support x ⊆ s) : HahnSeries.coeff (x * y) a = Finset.sum (Finset.addAntidiagonal hs (_ : Set.IsPwo (HahnSeries.support y)) a) fun ij => HahnSeries.coeff x ij.1 * HahnSeries.coeff y ij.2

instance HahnSeries.instDistribHahnSeriesToPartialOrderToZeroToMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] : Distrib (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.single_mul_coeff_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} : HahnSeries.coeff (↑(HahnSeries.single b) r * x) (a + b) = r * HahnSeries.coeff x a

theorem HahnSeries.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} : HahnSeries.coeff (x * ↑(HahnSeries.single b) r) (a + b) = HahnSeries.coeff x a * r

@[simp]

theorem HahnSeries.mul_single_zero_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (x * ↑(HahnSeries.single 0) r) a = HahnSeries.coeff x a * r

theorem HahnSeries.single_zero_mul_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} : HahnSeries.coeff (↑(HahnSeries.single 0) r * x) a = r * HahnSeries.coeff x a

@[simp]

theorem HahnSeries.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {r : R} {x : HahnSeries Γ R} : ↑(HahnSeries.single 0) r * x = r • x

theorem HahnSeries.support_mul_subset_add_support {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} : HahnSeries.support (x * y) ⊆ HahnSeries.support x + HahnSeries.support y

theorem HahnSeries.mul_coeff_order_add_order {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (y : HahnSeries Γ R) : HahnSeries.coeff (x * y) (HahnSeries.order x + HahnSeries.order y) = HahnSeries.coeff x (HahnSeries.order x) * HahnSeries.coeff y (HahnSeries.order y)

instance HahnSeries.instNonUnitalNonAssocSemiringHahnSeriesToPartialOrderToZeroToMulZeroClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonUnitalSemiringHahnSeriesToPartialOrderToZeroToSemigroupWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalSemiring R] : NonUnitalSemiring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonAssocSemiringHahnSeriesToPartialOrderToZeroToMulZeroOneClass {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : NonAssocSemiring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] : Semiring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonUnitalCommSemiringHahnSeriesToPartialOrderToZeroToSemigroupWithZeroToNonUnitalSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalCommSemiring R] : NonUnitalCommSemiring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instCommSemiringHahnSeriesToPartialOrderToZeroToCommMonoidWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] : CommSemiring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonUnitalNonAssocRingHahnSeriesToPartialOrderToZeroToMulZeroClassToNonUnitalNonAssocSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonUnitalRingHahnSeriesToPartialOrderToZeroToSemigroupWithZeroToNonUnitalSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalRing R] : NonUnitalRing (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonAssocRingHahnSeriesToPartialOrderToZeroToMulZeroOneClassToNonAssocSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocRing R] : NonAssocRing (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instRingHahnSeriesToPartialOrderToZeroToMonoidWithZeroToSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Ring R] : Ring (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNonUnitalCommRingHahnSeriesToPartialOrderToZeroToSemigroupWithZeroToNonUnitalSemiringToNonUnitalCommSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalCommRing R] : NonUnitalCommRing (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instCommRingHahnSeriesToPartialOrderToZeroToCommMonoidWithZeroToCommSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommRing R] : CommRing (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instNoZeroDivisorsHahnSeriesToPartialOrderToOrderedCancelAddCommMonoidToZeroToMulZeroClassInstMulHahnSeriesToPartialOrderToZeroToMulZeroClassInstZeroHahnSeries {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] : NoZeroDivisors (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.instIsDomainHahnSeriesToPartialOrderToOrderedCancelAddCommMonoidToZeroToMonoidWithZeroToSemiringInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZero {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] : IsDomain (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.order_mul {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {x : HahnSeries Γ R} {y : HahnSeries Γ R} (hx : x ≠ 0) (hy : y ≠ 0) : HahnSeries.order (x * y) = HahnSeries.order x + HahnSeries.order y

@[simp]

theorem HahnSeries.order_pow {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [Semiring R] [NoZeroDivisors R] (x : HahnSeries Γ R) (n : ℕ) : HahnSeries.order (x ^ n) = n • HahnSeries.order x

@[simp]

theorem HahnSeries.single_mul_single {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {a : Γ} {b : Γ} {r : R} {s : R} : ↑(HahnSeries.single a) r * ↑(HahnSeries.single b) s = ↑(HahnSeries.single (a + b)) (r * s)

@[simp]

theorem HahnSeries.C_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] (a : R) : ↑HahnSeries.C a = ↑(HahnSeries.single 0) a

def HahnSeries.C {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : R →+* HahnSeries Γ R

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

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.C_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : ↑HahnSeries.C 0 = 0

theorem HahnSeries.C_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : ↑HahnSeries.C 1 = 1

theorem HahnSeries.C_injective {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] : Function.Injective ↑HahnSeries.C

theorem HahnSeries.C_ne_zero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] {r : R} (h : r ≠ 0) : ↑HahnSeries.C r ≠ 0

theorem HahnSeries.order_C {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonAssocSemiring R] {r : R} : HahnSeries.order (↑HahnSeries.C r) = 0

theorem HahnSeries.C_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {r : R} {x : HahnSeries Γ R} : ↑HahnSeries.C r * x = r • x

theorem HahnSeries.embDomain_mul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ') (hf : ∀ (x y : Γ), ↑f (x + y) = ↑f x + ↑f y) (x : HahnSeries Γ R) (y : HahnSeries Γ R) : HahnSeries.embDomain f (x * y) = HahnSeries.embDomain f x * HahnSeries.embDomain f y

theorem HahnSeries.embDomain_one {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ ↪o Γ') (hf : ↑f 0 = 0) : HahnSeries.embDomain f 1 = 1

@[simp]

theorem HahnSeries.embDomainRingHom_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ↑f) (hf : ∀ (g g' : Γ), ↑f g ≤ ↑f g' ↔ g ≤ g') : ∀ (a : HahnSeries Γ R), ↑(HahnSeries.embDomainRingHom f hfi hf) a = HahnSeries.embDomain { toEmbedding := { toFun := ↑f, inj' := hfi }, map_rel_iff' := (_ : ∀ {a b : Γ}, ↑f a ≤ ↑f b ↔ a ≤ b) } a

def HahnSeries.embDomainRingHom {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] (f : Γ →+ Γ') (hfi : Function.Injective ↑f) (hf : ∀ (g g' : Γ), ↑f g ≤ ↑f g' ↔ g ≤ g') : HahnSeries Γ R →+* HahnSeries Γ' R

Extending the domain of Hahn series is a ring homomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.embDomainRingHom_C {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] {Γ' : Type u_3} [OrderedCancelAddCommMonoid Γ'] [NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective ↑f} {hf : ∀ (g g' : Γ), ↑f g ≤ ↑f g' ↔ g ≤ g'} {r : R} : ↑(HahnSeries.embDomainRingHom f hfi hf) (↑HahnSeries.C r) = ↑HahnSeries.C r

instance HahnSeries.instAlgebraHahnSeriesToPartialOrderToZeroToMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZero {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] : Algebra R (HahnSeries Γ A)

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.C_eq_algebraMap {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] : HahnSeries.C = algebraMap R (HahnSeries Γ R)

theorem HahnSeries.algebraMap_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] {r : R} : ↑(algebraMap R (HahnSeries Γ A)) r = ↑HahnSeries.C (↑(algebraMap R A) r)

instance HahnSeries.instNontrivialSubalgebraHahnSeriesToPartialOrderToZeroToCommMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZeroToSemiringInstAlgebraHahnSeriesToPartialOrderToZeroToMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZeroId {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] [Nontrivial Γ] [Nontrivial R] : Nontrivial (Subalgebra R (HahnSeries Γ R))

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.embDomainAlgHom_apply_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] {Γ' : Type u_4} [OrderedCancelAddCommMonoid Γ'] (f : Γ →+ Γ') (hfi : Function.Injective ↑f) (hf : ∀ (g g' : Γ), ↑f g ≤ ↑f g' ↔ g ≤ g') : ∀ (a : HahnSeries Γ A) (b : Γ'), HahnSeries.coeff (↑(HahnSeries.embDomainAlgHom f hfi hf) a) b = if h : ∃ x, ¬HahnSeries.coeff a x = 0 ∧ ↑f x = b then HahnSeries.coeff a (Classical.choose (_ : ∃ x, (fun x => ¬HahnSeries.coeff a x = 0 ∧ ↑f x = b) x)) else 0

def HahnSeries.embDomainAlgHom {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] {Γ' : Type u_4} [OrderedCancelAddCommMonoid Γ'] (f : Γ →+ Γ') (hfi : Function.Injective ↑f) (hf : ∀ (g g' : Γ), ↑f g ≤ ↑f g' ↔ g ≤ g') : HahnSeries Γ A →ₐ[R] HahnSeries Γ' A

Extending the domain of Hahn series is an algebra homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.toPowerSeries_apply {R : Type u_2} [Semiring R] (f : HahnSeries ℕ R) : ↑HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff

@[simp]

theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] (f : PowerSeries R) (n : ℕ) : HahnSeries.coeff (↑(RingEquiv.symm HahnSeries.toPowerSeries) f) n = ↑(PowerSeries.coeff R n) f

def HahnSeries.toPowerSeries {R : Type u_2} [Semiring R] : HahnSeries ℕ R ≃+* PowerSeries R

The ring HahnSeries ℕ R is isomorphic to PowerSeries R.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.coeff_toPowerSeries {R : Type u_2} [Semiring R] {f : HahnSeries ℕ R} {n : ℕ} : ↑(PowerSeries.coeff R n) (↑HahnSeries.toPowerSeries f) = HahnSeries.coeff f n

theorem HahnSeries.coeff_toPowerSeries_symm {R : Type u_2} [Semiring R] {f : PowerSeries R} {n : ℕ} : HahnSeries.coeff (↑(RingEquiv.symm HahnSeries.toPowerSeries) f) n = ↑(PowerSeries.coeff R n) f

def HahnSeries.ofPowerSeries (Γ : Type u_1) (R : Type u_2) [Semiring R] [StrictOrderedSemiring Γ] : PowerSeries R →+* HahnSeries Γ R

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

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.ofPowerSeries_injective {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] : Function.Injective ↑(HahnSeries.ofPowerSeries Γ R)

theorem HahnSeries.ofPowerSeries_apply {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] (x : PowerSeries R) : ↑(HahnSeries.ofPowerSeries Γ R) 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} [Semiring R] [StrictOrderedSemiring Γ] (x : PowerSeries R) (n : ℕ) : HahnSeries.coeff (↑(HahnSeries.ofPowerSeries Γ R) x) ↑n = ↑(PowerSeries.coeff R n) x

@[simp]

theorem HahnSeries.ofPowerSeries_C {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] (r : R) : ↑(HahnSeries.ofPowerSeries Γ R) (↑(PowerSeries.C R) r) = ↑HahnSeries.C r

@[simp]

theorem HahnSeries.ofPowerSeries_X {Γ : Type u_1} {R : Type u_2} [Semiring R] [StrictOrderedSemiring Γ] : ↑(HahnSeries.ofPowerSeries Γ R) PowerSeries.X = ↑(HahnSeries.single 1) 1

@[simp]

theorem HahnSeries.ofPowerSeries_X_pow {Γ : Type u_1} [StrictOrderedSemiring Γ] {R : Type u_3} [CommSemiring R] (n : ℕ) : ↑(HahnSeries.ofPowerSeries Γ R) (PowerSeries.X ^ n) = ↑(HahnSeries.single ↑n) 1

@[simp]

theorem HahnSeries.toMvPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] {σ : Type u_3} [Fintype σ] (f : MvPowerSeries σ R) : (↑(RingEquiv.symm HahnSeries.toMvPowerSeries) f).coeff = f

@[simp]

theorem HahnSeries.toMvPowerSeries_apply {R : Type u_2} [Semiring R] {σ : Type u_3} [Fintype σ] (f : HahnSeries (σ →₀ ℕ) R) : ∀ (a : σ →₀ ℕ), ↑HahnSeries.toMvPowerSeries f a = HahnSeries.coeff f a

def HahnSeries.toMvPowerSeries {R : Type u_2} [Semiring R] {σ : Type u_3} [Fintype σ] : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R

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.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.coeff_toMvPowerSeries {R : Type u_2} [Semiring R] {σ : Type u_3} [Fintype σ] {f : HahnSeries (σ →₀ ℕ) R} {n : σ →₀ ℕ} : ↑(MvPowerSeries.coeff R n) (↑HahnSeries.toMvPowerSeries f) = HahnSeries.coeff f n

theorem HahnSeries.coeff_toMvPowerSeries_symm {R : Type u_2} [Semiring R] {σ : Type u_3} [Fintype σ] {f : MvPowerSeries σ R} {n : σ →₀ ℕ} : HahnSeries.coeff (↑(RingEquiv.symm HahnSeries.toMvPowerSeries) f) n = ↑(MvPowerSeries.coeff R n) f

@[simp]

theorem HahnSeries.toPowerSeriesAlg_symm_apply_coeff (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] (f : PowerSeries A) (n : ℕ) : HahnSeries.coeff (↑(AlgEquiv.symm (HahnSeries.toPowerSeriesAlg R)) f) n = ↑(PowerSeries.coeff A n) f

@[simp]

theorem HahnSeries.toPowerSeriesAlg_apply (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] (f : HahnSeries ℕ A) : ↑(HahnSeries.toPowerSeriesAlg R) f = PowerSeries.mk f.coeff

def HahnSeries.toPowerSeriesAlg (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] : HahnSeries ℕ A ≃ₐ[R] PowerSeries A

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

def HahnSeries.ofPowerSeriesAlg (Γ : Type u_1) (R : Type u_2) [CommSemiring R] {A : Type u_3} [Semiring A] [Algebra R A] [StrictOrderedSemiring Γ] : PowerSeries A →ₐ[R] HahnSeries Γ A

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

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.powerSeriesAlgebra (Γ : Type u_1) (R : Type u_2) [CommSemiring R] [StrictOrderedSemiring Γ] {S : Type u_4} [CommSemiring S] [Algebra S (PowerSeries R)] : Algebra S (HahnSeries Γ R)

Equations

• HahnSeries.powerSeriesAlgebra Γ R = RingHom.toAlgebra (RingHom.comp (HahnSeries.ofPowerSeries Γ R) (algebraMap S (PowerSeries R)))

theorem HahnSeries.algebraMap_apply' (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [StrictOrderedSemiring Γ] {S : Type u_4} [CommSemiring S] [Algebra S (PowerSeries R)] (x : S) : ↑(algebraMap S (HahnSeries Γ R)) x = ↑(HahnSeries.ofPowerSeries Γ R) (↑(algebraMap S (PowerSeries R)) x)

@[simp]

theorem Polynomial.algebraMap_hahnSeries_apply (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [StrictOrderedSemiring Γ] (f : Polynomial R) : ↑(algebraMap (Polynomial R) (HahnSeries Γ R)) f = ↑(HahnSeries.ofPowerSeries Γ R) ↑f

theorem Polynomial.algebraMap_hahnSeries_injective (Γ : Type u_1) {R : Type u_2} [CommSemiring R] [StrictOrderedSemiring Γ] : Function.Injective ↑(algebraMap (Polynomial R) (HahnSeries Γ R))

def HahnSeries.addVal (Γ : Type u_1) (R : Type u_2) [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] : AddValuation (HahnSeries Γ R) (WithTop Γ)

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

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.addVal_apply {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} : ↑(HahnSeries.addVal Γ R) x = if x = 0 then ⊤ else ↑(HahnSeries.order x)

@[simp]

theorem HahnSeries.addVal_apply_of_ne {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (hx : x ≠ 0) : ↑(HahnSeries.addVal Γ R) x = ↑(HahnSeries.order x)

theorem HahnSeries.addVal_le_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} {g : Γ} (h : HahnSeries.coeff x g ≠ 0) : ↑(HahnSeries.addVal Γ R) x ≤ ↑g

theorem HahnSeries.isPwo_iUnion_support_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [Ring R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < ↑(HahnSeries.addVal Γ R) x) : Set.IsPwo (⋃ n, HahnSeries.support (x ^ n))

structure HahnSeries.SummableFamily (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [AddCommMonoid R] (α : Type u_3) : Type (max (max u_1 u_2) u_3)

• toFun : α → HahnSeries Γ R
• isPwo_iUnion_support' : Set.IsPwo (⋃ a, HahnSeries.support (HahnSeries.SummableFamily.toFun s a))
• finite_co_support' : ∀ (g : Γ), Set.Finite {a | HahnSeries.coeff (HahnSeries.SummableFamily.toFun s a) g ≠ 0}

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.

instance HahnSeries.SummableFamily.instFunLikeSummableFamilyHahnSeriesToZeroToAddMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : FunLike (HahnSeries.SummableFamily Γ R α) α fun x => HahnSeries Γ R

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.SummableFamily.isPwo_iUnion_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) : Set.IsPwo (⋃ a, HahnSeries.support (↑s a))

theorem HahnSeries.SummableFamily.finite_co_support {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) (g : Γ) : Set.Finite (Function.support fun a => HahnSeries.coeff (↑s a) g)

theorem HahnSeries.SummableFamily.coe_injective {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Function.Injective FunLike.coe

theorem HahnSeries.SummableFamily.ext {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} (h : ∀ (a : α), ↑s a = ↑t a) : s = t

instance HahnSeries.SummableFamily.instAddSummableFamily {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Add (HahnSeries.SummableFamily Γ R α)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.SummableFamily.instZeroSummableFamily {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Zero (HahnSeries.SummableFamily Γ R α)

Equations

• One or more equations did not get rendered due to their size.

instance HahnSeries.SummableFamily.instInhabitedSummableFamily {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : Inhabited (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instInhabitedSummableFamily = { default := 0 }

@[simp]

theorem HahnSeries.SummableFamily.coe_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : ↑(s + t) = ↑s + ↑t

theorem HahnSeries.SummableFamily.add_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} {a : α} : ↑(s + t) a = ↑s a + ↑t a

@[simp]

theorem HahnSeries.SummableFamily.coe_zero {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : ↑0 = 0

theorem HahnSeries.SummableFamily.zero_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {a : α} : ↑0 a = 0

instance HahnSeries.SummableFamily.instAddCommMonoidSummableFamily {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} : AddCommMonoid (HahnSeries.SummableFamily Γ R α)

Equations

• HahnSeries.SummableFamily.instAddCommMonoidSummableFamily = AddCommMonoid.mk (_ : ∀ (s t : HahnSeries.SummableFamily Γ R α), s + t = t + s)

def HahnSeries.SummableFamily.hsum {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) : HahnSeries Γ R

The infinite sum of a SummableFamily of Hahn series.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.hsum_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {g : Γ} : HahnSeries.coeff (HahnSeries.SummableFamily.hsum s) g = ∑ᶠ (i : α), HahnSeries.coeff (↑s i) g

theorem HahnSeries.SummableFamily.support_hsum_subset {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} : HahnSeries.support (HahnSeries.SummableFamily.hsum s) ⊆ ⋃ a, HahnSeries.support (↑s a)

@[simp]

theorem HahnSeries.SummableFamily.hsum_add {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : HahnSeries.SummableFamily.hsum (s + t) = HahnSeries.SummableFamily.hsum s + HahnSeries.SummableFamily.hsum t

instance HahnSeries.SummableFamily.instAddCommGroupSummableFamilyToAddCommMonoid {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} : AddCommGroup (HahnSeries.SummableFamily Γ R α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.coe_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} : ↑(-s) = -↑s

theorem HahnSeries.SummableFamily.neg_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {a : α} : ↑(-s) a = -↑s a

@[simp]

theorem HahnSeries.SummableFamily.coe_sub {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : ↑(s - t) = ↑s - ↑t

theorem HahnSeries.SummableFamily.sub_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommGroup R] {α : Type u_3} {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} {a : α} : ↑(s - t) a = ↑s a - ↑t a

instance HahnSeries.SummableFamily.instSMulHahnSeriesToPartialOrderToZeroToMonoidWithZeroSummableFamilyToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiring {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} : SMul (HahnSeries Γ R) (HahnSeries.SummableFamily Γ R α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.smul_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ R α} {a : α} : ↑(x • s) a = x * ↑s a

instance HahnSeries.SummableFamily.instModuleHahnSeriesToPartialOrderToZeroToMonoidWithZeroSummableFamilyToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringInstSemiringHahnSeriesToPartialOrderToZeroToMonoidWithZeroInstAddCommMonoidSummableFamily {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} : Module (HahnSeries Γ R) (HahnSeries.SummableFamily Γ R α)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.hsum_smul {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ R α} : HahnSeries.SummableFamily.hsum (x • s) = x * HahnSeries.SummableFamily.hsum s

@[simp]

theorem HahnSeries.SummableFamily.lsum_apply {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} (s : HahnSeries.SummableFamily Γ R α) : ↑HahnSeries.SummableFamily.lsum s = HahnSeries.SummableFamily.hsum s

def HahnSeries.SummableFamily.lsum {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Semiring R] {α : Type u_3} : HahnSeries.SummableFamily Γ R α →ₗ[HahnSeries Γ R] HahnSeries Γ R

The summation of a summable_family as a LinearMap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.hsum_sub {Γ : Type u_1} [OrderedCancelAddCommMonoid Γ] {α : Type u_3} {R : Type u_4} [Ring R] {s : HahnSeries.SummableFamily Γ R α} {t : HahnSeries.SummableFamily Γ R α} : HahnSeries.SummableFamily.hsum (s - t) = HahnSeries.SummableFamily.hsum s - HahnSeries.SummableFamily.hsum t

def HahnSeries.SummableFamily.ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} (f : α →₀ HahnSeries Γ R) : HahnSeries.SummableFamily Γ R α

A family with only finitely many nonzero elements is summable.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.coe_ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {f : α →₀ HahnSeries Γ R} : ↑(HahnSeries.SummableFamily.ofFinsupp f) = ↑f

@[simp]

theorem HahnSeries.SummableFamily.hsum_ofFinsupp {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {f : α →₀ HahnSeries Γ R} : HahnSeries.SummableFamily.hsum (HahnSeries.SummableFamily.ofFinsupp f) = Finsupp.sum f fun x => id

def HahnSeries.SummableFamily.embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) : HahnSeries.SummableFamily Γ R β

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

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.SummableFamily.embDomain_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β} : ↑(HahnSeries.SummableFamily.embDomain s f) b = if h : b ∈ Set.range ↑f then ↑s (Classical.choose h) else 0

@[simp]

theorem HahnSeries.SummableFamily.embDomain_image {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {a : α} : ↑(HahnSeries.SummableFamily.embDomain s f) (↑f a) = ↑s a

@[simp]

theorem HahnSeries.SummableFamily.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β} (h : ¬b ∈ Set.range ↑f) : ↑(HahnSeries.SummableFamily.embDomain s f) b = 0

@[simp]

theorem HahnSeries.SummableFamily.hsum_embDomain {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_3} {β : Type u_4} (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) : HahnSeries.SummableFamily.hsum (HahnSeries.SummableFamily.embDomain s f) = HahnSeries.SummableFamily.hsum s

def HahnSeries.SummableFamily.powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] (x : HahnSeries Γ R) (hx : 0 < ↑(HahnSeries.addVal Γ R) x) : HahnSeries.SummableFamily Γ R ℕ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HahnSeries.SummableFamily.coe_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < ↑(HahnSeries.addVal Γ R) x) : ↑(HahnSeries.SummableFamily.powers x hx) = HPow.hPow x

theorem HahnSeries.SummableFamily.embDomain_succ_smul_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < ↑(HahnSeries.addVal Γ R) x) : HahnSeries.SummableFamily.embDomain (x • HahnSeries.SummableFamily.powers x hx) { toFun := Nat.succ, inj' := Nat.succ_injective } = HahnSeries.SummableFamily.powers x hx - HahnSeries.SummableFamily.ofFinsupp fun₀ | 0 => 1

theorem HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers {Γ : Type u_1} {R : Type u_2} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} (hx : 0 < ↑(HahnSeries.addVal Γ R) x) : (1 - x) * HahnSeries.SummableFamily.hsum (HahnSeries.SummableFamily.powers x hx) = 1

theorem HahnSeries.unit_aux {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R] (x : HahnSeries Γ R) {r : R} (hr : r * HahnSeries.coeff x (HahnSeries.order x) = 1) : 0 < ↑(HahnSeries.addVal Γ R) (1 - ↑HahnSeries.C r * ↑(HahnSeries.single (-HahnSeries.order x)) 1 * x)

theorem HahnSeries.isUnit_iff {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} : IsUnit x ↔ IsUnit (HahnSeries.coeff x (HahnSeries.order x))

instance HahnSeries.instFieldHahnSeriesToPartialOrderToOrderedAddCommGroupToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield {Γ : Type u_1} {R : Type u_2} [LinearOrderedAddCommGroup Γ] [Field R] : Field (HahnSeries Γ R)

Equations

• One or more equations did not get rendered due to their size.