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 : 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)

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.

coeff : Γ → R
isPWO_support' : Set.IsPWO (Function.support self.coeff)

Instances For

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

Instances For

@[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 ↔ x.coeff 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

(_ : Subsingleton (HahnSeries Γ R)) = (_ : Subsingleton (HahnSeries Γ R))

@[simp]

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

0.coeff 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 : x.coeff 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.

Instances For

@[simp]

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

((HahnSeries.single a) r).coeff 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.single a) r).coeff b = 0

theorem HahnSeries.single_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] {a : Γ} {b : Γ} {r : R} :

((HahnSeries.single a) r).coeff 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

(_ : Nontrivial (HahnSeries Γ R)) = (_ : Nontrivial (HahnSeries Γ R))

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))

Instances For

@[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) :

x.coeff (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 : x.coeff 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) :

x.coeff 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.

Instances For

@[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.embDomain f x).coeff (f a) = x.coeff 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.embDomain { toEmbedding := { toFun := f, inj' := hfi }, map_rel_iff' := (_ : ∀ {a b : Γ}, f a ≤ f b ↔ a ≤ b) } x).coeff (f a) = x.coeff 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.embDomain f x).coeff 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.embDomain f x).coeff 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 : HahnSeries Γ R) => { 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 : Γ} :

(x + y).coeff a = x.coeff a + y.coeff 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} [Zero Γ] [LinearOrder Γ] {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_coeff {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (a : Γ) (r : R) (j : Γ) :

((HahnSeries.single.addMonoidHom a) r).coeff j = Pi.single a r j

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.

Instances For

@[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 = f.coeff 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.

Instances For

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 : Γ} :

(-x).coeff a = -x.coeff 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 : Γ} :

(x - y).coeff a = x.coeff a - y.coeff 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 : R) (x : HahnSeries Γ V) => { 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 : Γ} :

(r • x).coeff a = r • x.coeff 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.

theorem HahnSeries.order_smul_not_lt {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :

¬HahnSeries.order (r • x) < HahnSeries.order x

theorem HahnSeries.le_order_smul {R : Type u_2} {V : Type u_3} [Monoid R] [AddMonoid V] [DistribMulAction R V] {Γ : Type u_4} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :

HahnSeries.order x ≤ HahnSeries.order (r • x)

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

(_ : IsScalarTower R S (HahnSeries Γ V)) = (_ : IsScalarTower R S (HahnSeries Γ V))

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

(_ : SMulCommClass R S (HahnSeries Γ V)) = (_ : SMulCommClass R S (HahnSeries Γ V))

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] {V : Type u_3} [AddCommMonoid V] [Module R V] (a : Γ) :

∀ (a_1 : V), (HahnSeries.single.linearMap a) a_1 = (↑(HahnSeries.single.addMonoidHom a)).toFun a_1

def HahnSeries.single.linearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (a : Γ) :

V →ₗ[R] HahnSeries Γ V

single as a linear map

Equations

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

Instances For

@[simp]

theorem HahnSeries.coeff.linearMap_apply {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (g : Γ) :

∀ (a : HahnSeries Γ V), (HahnSeries.coeff.linearMap g) a = (↑(HahnSeries.coeff.addMonoidHom g)).toFun a

def HahnSeries.coeff.linearMap {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Semiring R] {V : Type u_3} [AddCommMonoid V] [Module R V] (g : Γ) :

HahnSeries Γ V →ₗ[R] V

coeff g as a linear map

Equations

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

Instances For

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.

Instances For

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

One (HahnSeries Γ R)

Equations

HahnSeries.instOneHahnSeriesToPartialOrderToOrderedAddCommMonoid = { one := (HahnSeries.single 0) 1 }

@[simp]

theorem HahnSeries.one_coeff {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [Zero R] [One R] {a : Γ} :

1.coeff 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.instMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass {Γ : 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 : Γ} :

(x * y).coeff a = Finset.sum (Finset.addAntidiagonal (_ : Set.IsPWO (HahnSeries.support x)) (_ : Set.IsPWO (HahnSeries.support y)) a) fun (ij : Γ × Γ) => x.coeff ij.1 * y.coeff 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) :

(x * y).coeff a = Finset.sum (Finset.addAntidiagonal (_ : Set.IsPWO (HahnSeries.support x)) hs a) fun (ij : Γ × Γ) => x.coeff ij.1 * y.coeff 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) :

(x * y).coeff a = Finset.sum (Finset.addAntidiagonal hs (_ : Set.IsPWO (HahnSeries.support y)) a) fun (ij : Γ × Γ) => x.coeff ij.1 * y.coeff ij.2

instance HahnSeries.instDistribHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass {Γ : 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.single b) r * x).coeff (a + b) = r * x.coeff a

theorem HahnSeries.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} :

(x * (HahnSeries.single b) r).coeff (a + b) = x.coeff 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 : Γ} :

(x * (HahnSeries.single 0) r).coeff a = x.coeff 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.single 0) r * x).coeff a = r * x.coeff 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) :

(x * y).coeff (HahnSeries.order x + HahnSeries.order y) = x.coeff (HahnSeries.order x) * y.coeff (HahnSeries.order y)

instance HahnSeries.instNonUnitalNonAssocSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClass {Γ : 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.instNonUnitalSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZero {Γ : 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.instNonAssocSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroOneClass {Γ : 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.instSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZero {Γ : 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.instNonUnitalCommSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiring {Γ : 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.instCommSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZero {Γ : 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.instNonUnitalNonAssocRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClassToNonUnitalNonAssocSemiring {Γ : 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.instNonUnitalRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiring {Γ : 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.instNonAssocRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroOneClassToNonAssocSemiring {Γ : 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.instRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroToSemiring {Γ : 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.instNonUnitalCommRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToSemigroupWithZeroToNonUnitalSemiringToNonUnitalCommSemiring {Γ : 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.instCommRingHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZeroToCommSemiring {Γ : 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.instNoZeroDivisorsHahnSeriesToPartialOrderToOrderedAddCommMonoidToLinearOrderedAddCommMonoidToZeroToMulZeroClassInstMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMulZeroClassToOrderedCancelAddCommMonoidInstZeroHahnSeries {R : Type u_2} {Γ : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [NonUnitalNonAssocSemiring R] [NoZeroDivisors R] :

NoZeroDivisors (HahnSeries Γ R)

Equations

(_ : NoZeroDivisors (HahnSeries Γ R)) = (_ : NoZeroDivisors (HahnSeries Γ R))

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

IsDomain (HahnSeries Γ R)

Equations

(_ : IsDomain (HahnSeries Γ R)) = (_ : IsDomain (HahnSeries Γ R))

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

Instances For

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.

Instances For

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.instAlgebraHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZero {Γ : 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.instNontrivialSubalgebraHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToCommMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroToSemiringInstAlgebraHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroId {Γ : Type u_1} {R : Type u_2} [OrderedCancelAddCommMonoid Γ] [CommSemiring R] [Nontrivial Γ] [Nontrivial R] :

Nontrivial (Subalgebra R (HahnSeries Γ R))

Equations

(_ : Nontrivial (Subalgebra R (HahnSeries Γ R))) = (_ : Nontrivial (Subalgebra R (HahnSeries Γ R)))

@[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.embDomainAlgHom f hfi hf) a).coeff b = if h : ∃ (x : Γ), ¬a.coeff x = 0 ∧ f x = b then a.coeff (Classical.choose (_ : ∃ (x : Γ), (fun (x : Γ) => ¬a.coeff 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.

Instances For

@[simp]

theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [Semiring R] (f : PowerSeries R) (n : ℕ) :

((RingEquiv.symm HahnSeries.toPowerSeries) f).coeff n = (PowerSeries.coeff R n) f

@[simp]

theorem HahnSeries.toPowerSeries_apply {R : Type u_2} [Semiring R] (f : HahnSeries ℕ R) :

HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff

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.

Instances For

theorem HahnSeries.coeff_toPowerSeries {R : Type u_2} [Semiring R] {f : HahnSeries ℕ R} {n : ℕ} :

(PowerSeries.coeff R n) (HahnSeries.toPowerSeries f) = f.coeff n

theorem HahnSeries.coeff_toPowerSeries_symm {R : Type u_2} [Semiring R] {f : PowerSeries R} {n : ℕ} :

((RingEquiv.symm HahnSeries.toPowerSeries) f).coeff 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.

Instances For

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.ofPowerSeries Γ R) x).coeff ↑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 = f.coeff 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.

Instances For

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) = f.coeff n

theorem HahnSeries.coeff_toMvPowerSeries_symm {R : Type u_2} [Semiring R] {σ : Type u_3} [Fintype σ] {f : MvPowerSeries σ R} {n : σ →₀ ℕ} :

((RingEquiv.symm HahnSeries.toMvPowerSeries) f).coeff 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 : ℕ) :

((AlgEquiv.symm (HahnSeries.toPowerSeriesAlg R)) f).coeff 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.

Instances For

@[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.ofPowerSeriesAlg Γ R) a).coeff 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.

Instances For

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.

Instances For

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 : x.coeff 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)

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.

toFun : α → HahnSeries Γ R
isPWO_iUnion_support' : Set.IsPWO (⋃ (a : α), HahnSeries.support (self.toFun a))
finite_co_support' : ∀ (g : Γ), Set.Finite {a : α | (self.toFun a).coeff g ≠ 0}

Instances For

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

FunLike (HahnSeries.SummableFamily Γ R α) α (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 : α) => (s a).coeff g)

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

Function.Injective DFunLike.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.

Instances For

@[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.SummableFamily.hsum s).coeff g = finsum fun (i : α) => (s i).coeff 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.instSMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroSummableFamilyToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiring {Γ : 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.instModuleHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroSummableFamilyToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroInstAddCommMonoidSummableFamily {Γ : 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.

Instances For

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

Instances For

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

Instances For

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.

Instances For

@[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 (Finsupp.single 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 * x.coeff (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 (x.coeff (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.