Cardinality of Hahn series #

We define HahnSeries.cardSupp as the cardinality of the support of a Hahn series, and find bounds for the cardinalities of different operations. We also build the subgroups, subrings, etc. of Hahn series bounded by a given infinite cardinal.

Cardinality function #

source

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

Cardinal.{u_1}

The cardinality of the support of a Hahn series.

Equations

Instances For

source

theorem HahnSeries.cardSupp_congr {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] [Zero S] {x : HahnSeries Γ R} {y : HahnSeries Γ S} (h : x.support = y.support) :

x.cardSupp = y.cardSupp

source

theorem HahnSeries.cardSupp_mono {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] [Zero S] {x : HahnSeries Γ R} {y : HahnSeries Γ S} (h : x.support ⊆ y.support) :

x.cardSupp ≤ y.cardSupp

source

@[simp]

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

cardSupp 0 = 0

source

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

((single a) r).cardSupp = 1

source

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

((single a) r).cardSupp ≤ 1

source

@[simp]

theorem HahnSeries.cardSupp_one_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] [One R] :

cardSupp 1 ≤ 1

source

@[simp]

theorem HahnSeries.cardSupp_one {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [Zero Γ] [One R] [NeZero 1] :

cardSupp 1 = 1

source

theorem HahnSeries.cardSupp_map_le {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] [Zero S] (x : HahnSeries Γ R) (f : ZeroHom R S) :

(x.map f).cardSupp ≤ x.cardSupp

source

theorem HahnSeries.cardSupp_truncLT_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [Zero R] [DecidableLT Γ] (x : HahnSeries Γ R) (c : Γ) :

((truncLT c) x).cardSupp ≤ x.cardSupp

source

theorem HahnSeries.cardSupp_smul_le {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [PartialOrder Γ] [Zero R] (s : S) (x : HahnSeries Γ R) [SMulZeroClass S R] :

(s • x).cardSupp ≤ x.cardSupp

source

theorem HahnSeries.cardSupp_neg_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [NegZeroClass R] (x : HahnSeries Γ R) :

(-x).cardSupp ≤ x.cardSupp

source

theorem HahnSeries.cardSupp_add_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddMonoid R] (x y : HahnSeries Γ R) :

(x + y).cardSupp ≤ x.cardSupp + y.cardSupp

source

@[simp]

theorem HahnSeries.cardSupp_neg {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] (x : HahnSeries Γ R) :

(-x).cardSupp = x.cardSupp

source

theorem HahnSeries.cardSupp_sub_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddGroup R] (x y : HahnSeries Γ R) :

(x - y).cardSupp ≤ x.cardSupp + y.cardSupp

source

theorem HahnSeries.cardSupp_mul_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x y : HahnSeries Γ R) :

(x * y).cardSupp ≤ x.cardSupp * y.cardSupp

source

theorem HahnSeries.cardSupp_single_mul_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (a : Γ) (r : R) :

((single a) r * x).cardSupp ≤ x.cardSupp

source

theorem HahnSeries.cardSupp_mul_single_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (a : Γ) (r : R) :

(x * (single a) r).cardSupp ≤ x.cardSupp

source

theorem HahnSeries.cardSupp_pow_le {Γ : Type u_1} {R : Type u_2} [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (x : HahnSeries Γ R) (n : ℕ) :

(x ^ n).cardSupp ≤ x.cardSupp ^ n

source

theorem HahnSeries.cardSupp_hsum_le {Γ : Type u_1} {R : Type u_2} {α : Type u_4} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) :

Cardinal.lift.{u_4, u_1} s.hsum.cardSupp ≤ Cardinal.sum fun (a : α) => (s a).cardSupp

source

theorem HahnSeries.cardSupp_hsum_powers_le {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) :

(SummableFamily.powers x).hsum.cardSupp ≤ max Cardinal.aleph0 x.cardSupp

source

theorem HahnSeries.cardSupp_inv_le {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] (x : HahnSeries Γ R) :

x⁻¹.cardSupp ≤ max Cardinal.aleph0 x.cardSupp

source

theorem HahnSeries.cardSupp_div_le {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] (x y : HahnSeries Γ R) :

(x / y).cardSupp ≤ x.cardSupp * max Cardinal.aleph0 y.cardSupp

Substructures #

source

def HahnSeries.cardSuppLTAddSubmonoid (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddMonoid R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] :

AddSubmonoid (HahnSeries Γ R)

The κ-bounded submonoid of Hahn series with less than κ terms.

Equations

Instances For

source

@[simp]

theorem HahnSeries.coe_cardSuppLTAddSubmonoid (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddMonoid R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] :

↑(cardSuppLTAddSubmonoid Γ R κ) = {x : HahnSeries Γ R | x.cardSupp < κ}

source

@[simp]

theorem HahnSeries.mem_cardSuppLTAddSubmonoid {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddMonoid R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R} :

x ∈ cardSuppLTAddSubmonoid Γ R κ ↔ x.cardSupp < κ

source

def HahnSeries.cardSuppLTAddSubgroup (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddGroup R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] :

AddSubgroup (HahnSeries Γ R)

The κ-bounded subgroup of Hahn series with less than κ terms.

Equations

Instances For

source

@[simp]

theorem HahnSeries.coe_cardSuppLTAddSubgroup (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddGroup R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] :

↑(cardSuppLTAddSubgroup Γ R κ) = {x : HahnSeries Γ R | x.cardSupp < κ}

source

@[simp]

theorem HahnSeries.mem_cardSuppLTAddSubgroup {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddGroup R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R} :

x ∈ cardSuppLTAddSubgroup Γ R κ ↔ x.cardSupp < κ

source

def HahnSeries.cardSuppLTSubring (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] :

Subring (HahnSeries Γ R)

The κ-bounded subring of Hahn series with less than κ terms.

Equations

Instances For

source

@[simp]

theorem HahnSeries.mem_cardSuppLTSubring {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [PartialOrder Γ] [AddCommMonoid Γ] [IsOrderedCancelAddMonoid Γ] [Ring R] [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R} :

x ∈ cardSuppLTSubring Γ R κ ↔ x.cardSupp < κ

source

def HahnSeries.cardSuppLTSubfield (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] :

Subfield (HahnSeries Γ R)

The κ-bounded subfield of Hahn series with less than κ terms.

Equations

Instances For

source

@[simp]

theorem HahnSeries.cardSuppLTSubfield_carrier (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] :

↑(cardSuppLTSubfield Γ R κ) = (cardSuppLTAddSubgroup Γ R κ).carrier

source

@[simp]

theorem HahnSeries.mem_cardSuppLTSubfield {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [LinearOrder Γ] [AddCommGroup Γ] [IsOrderedAddMonoid Γ] [Field R] [hκ : Fact (Cardinal.aleph0 < κ)] {x : HahnSeries Γ R} :

x ∈ cardSuppLTSubfield Γ R κ ↔ x.cardSupp < κ

Documentation

Mathlib.RingTheory.HahnSeries.Cardinal

Cardinality of Hahn series #

Cardinality function #

Substructures #