Archimedean classes of a linearly ordered group

This file defines archimedean classes of a given linearly ordered group. Archimedean classes measure to what extent the group fails to be Archimedean. For additive group, elements a and b in the same class are "equivalent" in the sense that there exist two natural numbers m and n such that |a| ≤ m • |b| and |b| ≤ n • |a|. An element a in a higher class than b is "infinitesimal" to b in the sense that n • |a| < |b| for all natural number n.

Main definitions

• ArchimedeanClass is the archimedean class for additive linearly ordered group.
• MulArchimedeanClass is the archimedean class for multiplicative linearly ordered group.
• ArchimedeanClass.orderHom and MulArchimedeanClass.orderHom are OrderHom over archimedean classes lifted from ordered group homomorphisms.
• ArchimedeanClass.ballAddSubgroup and MulArchimedeanClass.ballSubgroup are subgroups formed by an open interval of archimedean classes
• ArchimedeanClass.closedBallAddSubgroup and MulArchimedeanClass.closedBallSubgroup are subgroups formed by a closed interval of archimedean classes.

Main statements

The following theorems state that an ordered commutative group is (mul-)archimedean if and only if all non-identity elements belong to the same (Mul-)ArchimedeanClass:

• ArchimedeanClass.archimedean_of_mk_eq_mk / MulArchimedeanClass.mulArchimedean_of_mk_eq_mk
• ArchimedeanClass.mk_eq_mk_of_archimedean / MulArchimedeanClass.mk_eq_mk_of_mulArchimedean

Implementation notes

Archimedean classes are equipped with a linear order, where elements with smaller absolute value are placed in a higher classes by convention. Ordering backwards this way simplifies formalization of theorems such as the Hahn embedding theorem.

To naturally derive this order, we first define it on the underlying group via the type synonym (Mul-)ArchimedeanOrder, and define (Mul-)ArchimedeanClass as Antisymmetrization of the order.

def MulArchimedeanOrder (M : Type u_1) : Type u_1

Type synonym to equip a ordered group with a new Preorder defined by the infinitesimal order of elements. a is said less than b if b is infinitesimal comparing to a, or more precisely, ∀ n, |b|ₘ ^ n < |a|ₘ. If a and b are neither infinitesimal to each other, they are equivalent in this order.

Equations

• MulArchimedeanOrder M = M

def ArchimedeanOrder (M : Type u_1) : Type u_1

Type synonym to equip a ordered group with a new Preorder defined by the infinitesimal order of elements. a is said less than b if b is infinitesimal comparing to a, or more precisely, ∀ n, n • |b| < |a|. If a and b are neither infinitesimal to each other, they are equivalent in this order.

Equations

• ArchimedeanOrder M = M

def MulArchimedeanOrder.of {M : Type u_1} : M ≃ MulArchimedeanOrder M

Create a MulArchimedeanOrder element from the underlying type.

Equations

• MulArchimedeanOrder.of = Equiv.refl M

def ArchimedeanOrder.of {M : Type u_1} : M ≃ ArchimedeanOrder M

Create a ArchimedeanOrder element from the underlying type.

Equations

• ArchimedeanOrder.of = Equiv.refl M

def MulArchimedeanOrder.val {M : Type u_1} : MulArchimedeanOrder M ≃ M

Retrieve the underlying value from a MulArchimedeanOrder element.

Equations

• MulArchimedeanOrder.val = Equiv.refl (MulArchimedeanOrder M)

def ArchimedeanOrder.val {M : Type u_1} : ArchimedeanOrder M ≃ M

Retrieve the underlying value from a ArchimedeanOrder element.

Equations

• ArchimedeanOrder.val = Equiv.refl (ArchimedeanOrder M)

@[simp]

theorem MulArchimedeanOrder.of_symm_eq {M : Type u_1} : of.symm = val

@[simp]

theorem ArchimedeanOrder.of_symm_eq {M : Type u_1} : of.symm = val

@[simp]

theorem MulArchimedeanOrder.val_symm_eq {M : Type u_1} : val.symm = of

@[simp]

theorem ArchimedeanOrder.val_symm_eq {M : Type u_1} : val.symm = of

@[simp]

theorem MulArchimedeanOrder.of_val {M : Type u_1} (a : MulArchimedeanOrder M) : of (val a) = a

@[simp]

theorem ArchimedeanOrder.of_val {M : Type u_1} (a : ArchimedeanOrder M) : of (val a) = a

@[simp]

theorem MulArchimedeanOrder.val_of {M : Type u_1} (a : M) : val (of a) = a

@[simp]

theorem ArchimedeanOrder.val_of {M : Type u_1} (a : M) : val (of a) = a

instance MulArchimedeanOrder.instLE {M : Type u_1} [Group M] [Lattice M] : LE (MulArchimedeanOrder M)

Equations

• MulArchimedeanOrder.instLE = { le := fun (a b : MulArchimedeanOrder M) => ∃ (n : ℕ), mabs (MulArchimedeanOrder.val b) ≤ mabs (MulArchimedeanOrder.val a) ^ n }

instance ArchimedeanOrder.instLE {M : Type u_1} [AddGroup M] [Lattice M] : LE (ArchimedeanOrder M)

Equations

• ArchimedeanOrder.instLE = { le := fun (a b : ArchimedeanOrder M) => ∃ (n : ℕ), |ArchimedeanOrder.val b| ≤ n • |ArchimedeanOrder.val a| }

instance MulArchimedeanOrder.instLT {M : Type u_1} [Group M] [Lattice M] : LT (MulArchimedeanOrder M)

Equations

• MulArchimedeanOrder.instLT = { lt := fun (a b : MulArchimedeanOrder M) => ∀ (n : ℕ), mabs (MulArchimedeanOrder.val b) ^ n < mabs (MulArchimedeanOrder.val a) }

instance ArchimedeanOrder.instLT {M : Type u_1} [AddGroup M] [Lattice M] : LT (ArchimedeanOrder M)

Equations

• ArchimedeanOrder.instLT = { lt := fun (a b : ArchimedeanOrder M) => ∀ (n : ℕ), n • |ArchimedeanOrder.val b| < |ArchimedeanOrder.val a| }

theorem MulArchimedeanOrder.le_def {M : Type u_1} [Group M] [Lattice M] {a b : MulArchimedeanOrder M} : a ≤ b ↔ ∃ (n : ℕ), mabs (val b) ≤ mabs (val a) ^ n

theorem ArchimedeanOrder.le_def {M : Type u_1} [AddGroup M] [Lattice M] {a b : ArchimedeanOrder M} : a ≤ b ↔ ∃ (n : ℕ), |val b| ≤ n • |val a|

theorem MulArchimedeanOrder.lt_def {M : Type u_1} [Group M] [Lattice M] {a b : MulArchimedeanOrder M} : a < b ↔ ∀ (n : ℕ), mabs (val b) ^ n < mabs (val a)

theorem ArchimedeanOrder.lt_def {M : Type u_1} [AddGroup M] [Lattice M] {a b : ArchimedeanOrder M} : a < b ↔ ∀ (n : ℕ), n • |val b| < |val a|

instance MulArchimedeanOrder.instPreorder {M : Type u_2} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Preorder (MulArchimedeanOrder M)

Equations

• MulArchimedeanOrder.instPreorder = { toLE := MulArchimedeanOrder.instLE, toLT := MulArchimedeanOrder.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance ArchimedeanOrder.instPreorder {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Preorder (ArchimedeanOrder M)

Equations

• ArchimedeanOrder.instPreorder = { toLE := ArchimedeanOrder.instLE, toLT := ArchimedeanOrder.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance MulArchimedeanOrder.instIsTotalLe {M : Type u_2} [CommGroup M] [LinearOrder M] : IsTotal (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) => x1 ≤ x2

instance ArchimedeanOrder.instIsTotalLe {M : Type u_2} [AddCommGroup M] [LinearOrder M] : IsTotal (ArchimedeanOrder M) fun (x1 x2 : ArchimedeanOrder M) => x1 ≤ x2

noncomputable def MulArchimedeanOrder.orderHom {M : Type u_2} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_3} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) : MulArchimedeanOrder M →o MulArchimedeanOrder N

An OrderMonoidHom can be made to an OrderHom between their MulArchimedeanOrder.

Equations

• MulArchimedeanOrder.orderHom f = { toFun := fun (a : MulArchimedeanOrder M) => MulArchimedeanOrder.of (f (MulArchimedeanOrder.val a)), monotone' := ⋯ }

noncomputable def ArchimedeanOrder.orderHom {M : Type u_2} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_3} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) : ArchimedeanOrder M →o ArchimedeanOrder N

An OrderAddMonoidHom can be made to an OrderHom between their ArchimedeanOrder.

Equations

• ArchimedeanOrder.orderHom f = { toFun := fun (a : ArchimedeanOrder M) => ArchimedeanOrder.of (f (ArchimedeanOrder.val a)), monotone' := ⋯ }

def MulArchimedeanClass (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Type u_1

MulArchimedeanClass M is the quotient of the group M by multiplicative archimedean equivalence, where two elements a and b are in the same class iff (∃ m : ℕ, |b|ₘ ≤ |a|ₘ ^ m) ∧ (∃ n : ℕ, |a|ₘ ≤ |b|ₘ ^ n).

Equations

• MulArchimedeanClass M = Antisymmetrization (MulArchimedeanOrder M) fun (x1 x2 : MulArchimedeanOrder M) => x1 ≤ x2

def ArchimedeanClass (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Type u_1

ArchimedeanClass M is the quotient of the additive group M by additive archimedean equivalence, where two elements a and b are in the same class iff (∃ m : ℕ, |b| ≤ m • |a|) ∧ (∃ n : ℕ, |a| ≤ n • |b|).

Equations

• ArchimedeanClass M = Antisymmetrization (ArchimedeanOrder M) fun (x1 x2 : ArchimedeanOrder M) => x1 ≤ x2

def MulArchimedeanClass.mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) : MulArchimedeanClass M

The archimedean class of a given element.

Equations

• MulArchimedeanClass.mk a = toAntisymmetrization (fun (x1 x2 : MulArchimedeanOrder M) => x1 ≤ x2) (MulArchimedeanOrder.of a)

def ArchimedeanClass.mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) : ArchimedeanClass M

The archimedean class of a given element.

Equations

• ArchimedeanClass.mk a = toAntisymmetrization (fun (x1 x2 : ArchimedeanOrder M) => x1 ≤ x2) (ArchimedeanOrder.of a)

theorem MulArchimedeanClass.ind {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {motive : MulArchimedeanClass M → Prop} (mk : ∀ (a : M), motive (mk a)) (x : MulArchimedeanClass M) : motive x

An induction principle for MulArchimedeanClass.

theorem ArchimedeanClass.ind {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {motive : ArchimedeanClass M → Prop} (mk : ∀ (a : M), motive (mk a)) (x : ArchimedeanClass M) : motive x

An induction principle for ArchimedeanClass

theorem MulArchimedeanClass.forall {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {p : MulArchimedeanClass M → Prop} : (∀ (A : MulArchimedeanClass M), p A) ↔ ∀ (a : M), p (mk a)

theorem ArchimedeanClass.forall {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {p : ArchimedeanClass M → Prop} : (∀ (A : ArchimedeanClass M), p A) ↔ ∀ (a : M), p (mk a)

theorem MulArchimedeanClass.mk_surjective (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Function.Surjective mk

theorem ArchimedeanClass.mk_surjective (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Function.Surjective mk

@[simp]

theorem MulArchimedeanClass.range_mk (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Set.range mk = Set.univ

@[simp]

theorem ArchimedeanClass.range_mk (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Set.range mk = Set.univ

theorem MulArchimedeanClass.mk_eq_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} : mk a = mk b ↔ (∃ (m : ℕ), mabs b ≤ mabs a ^ m) ∧ ∃ (n : ℕ), mabs a ≤ mabs b ^ n

theorem ArchimedeanClass.mk_eq_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} : mk a = mk b ↔ (∃ (m : ℕ), |b| ≤ m • |a|) ∧ ∃ (n : ℕ), |a| ≤ n • |b|

def MulArchimedeanClass.lift {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} (f : M → α) (h : ∀ (a b : M), mk a = mk b → f a = f b) : MulArchimedeanClass M → α

Lift a M → α function to MulArchimedeanClass M → α.

Equations

• MulArchimedeanClass.lift f h = Quotient.lift f ⋯

def ArchimedeanClass.lift {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} (f : M → α) (h : ∀ (a b : M), mk a = mk b → f a = f b) : ArchimedeanClass M → α

Lift a M → α function to ArchimedeanClass M → α.

Equations

• ArchimedeanClass.lift f h = Quotient.lift f ⋯

@[simp]

theorem MulArchimedeanClass.lift_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} (f : M → α) (h : ∀ (a b : M), mk a = mk b → f a = f b) (a : M) : lift f h (mk a) = f a

@[simp]

theorem ArchimedeanClass.lift_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} (f : M → α) (h : ∀ (a b : M), mk a = mk b → f a = f b) (a : M) : lift f h (mk a) = f a

def MulArchimedeanClass.lift₂ {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} (f : M → M → α) (h : ∀ (a₁ b₁ a₂ b₂ : M), mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂) : MulArchimedeanClass M → MulArchimedeanClass M → α

Lift a M → M → α function to MulArchimedeanClass M → MulArchimedeanClass M → α.

Equations

• MulArchimedeanClass.lift₂ f h = Quotient.lift₂ f ⋯

def ArchimedeanClass.lift₂ {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} (f : M → M → α) (h : ∀ (a₁ b₁ a₂ b₂ : M), mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂) : ArchimedeanClass M → ArchimedeanClass M → α

Lift a M → M → α function to ArchimedeanClass M → ArchimedeanClass M → α.

Equations

• ArchimedeanClass.lift₂ f h = Quotient.lift₂ f ⋯

@[simp]

theorem MulArchimedeanClass.lift₂_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} (f : M → M → α) (h : ∀ (a₁ b₁ a₂ b₂ : M), mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂) (a b : M) : lift₂ f h (mk a) (mk b) = f a b

@[simp]

theorem ArchimedeanClass.lift₂_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} (f : M → M → α) (h : ∀ (a₁ b₁ a₂ b₂ : M), mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂) (a b : M) : lift₂ f h (mk a) (mk b) = f a b

noncomputable def MulArchimedeanClass.out {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (A : MulArchimedeanClass M) : M

Choose a representative element from a given archimedean class.

Equations

• A.out = MulArchimedeanOrder.val (Quotient.out A)

noncomputable def ArchimedeanClass.out {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (A : ArchimedeanClass M) : M

Choose a representative element from a given archimedean class.

Equations

• A.out = ArchimedeanOrder.val (Quotient.out A)

@[simp]

theorem MulArchimedeanClass.mk_out {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (A : MulArchimedeanClass M) : mk A.out = A

@[simp]

theorem ArchimedeanClass.mk_out {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (A : ArchimedeanClass M) : mk A.out = A

@[simp]

theorem MulArchimedeanClass.mk_inv {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) : mk a⁻¹ = mk a

@[simp]

theorem ArchimedeanClass.mk_neg {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) : mk (-a) = mk a

theorem MulArchimedeanClass.mk_div_comm {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a b : M) : mk (a / b) = mk (b / a)

theorem ArchimedeanClass.mk_sub_comm {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a b : M) : mk (a - b) = mk (b - a)

@[simp]

theorem MulArchimedeanClass.mk_mabs {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) : mk (mabs a) = mk a

@[simp]

theorem ArchimedeanClass.mk_abs {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) : mk |a| = mk a

noncomputable instance MulArchimedeanClass.instLinearOrder {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : LinearOrder (MulArchimedeanClass M)

Equations

• MulArchimedeanClass.instLinearOrder = id inferInstance

noncomputable instance ArchimedeanClass.instLinearOrder {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : LinearOrder (ArchimedeanClass M)

Equations

• ArchimedeanClass.instLinearOrder = id inferInstance

theorem MulArchimedeanClass.mk_le_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} : mk a ≤ mk b ↔ ∃ (n : ℕ), mabs b ≤ mabs a ^ n

theorem ArchimedeanClass.mk_le_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} : mk a ≤ mk b ↔ ∃ (n : ℕ), |b| ≤ n • |a|

theorem MulArchimedeanClass.mk_lt_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} : mk a < mk b ↔ ∀ (n : ℕ), mabs b ^ n < mabs a

theorem ArchimedeanClass.mk_lt_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} : mk a < mk b ↔ ∀ (n : ℕ), n • |b| < |a|

instance MulArchimedeanClass.instOrderTop {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : OrderTop (MulArchimedeanClass M)

1 is in its own class (see MulArchimedeanClass.mk_eq_top_iff), which is also the largest class.

Equations

• MulArchimedeanClass.instOrderTop = { top := MulArchimedeanClass.mk 1, le_top := ⋯ }

instance ArchimedeanClass.instOrderTop {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : OrderTop (ArchimedeanClass M)

0 is in its own class (see ArchimedeanClass.mk_eq_top_iff), which is also the largest class.

Equations

• ArchimedeanClass.instOrderTop = { top := ArchimedeanClass.mk 0, le_top := ⋯ }

@[simp]

theorem MulArchimedeanClass.mk_one (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : mk 1 = ⊤

@[simp]

theorem ArchimedeanClass.mk_zero (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : mk 0 = ⊤

@[simp]

theorem MulArchimedeanClass.mk_eq_top_iff {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} : mk a = ⊤ ↔ a = 1

@[simp]

theorem ArchimedeanClass.mk_eq_top_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} : mk a = ⊤ ↔ a = 0

@[simp]

theorem MulArchimedeanClass.top_eq_mk_iff {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} : ⊤ = mk a ↔ a = 1

@[simp]

theorem ArchimedeanClass.top_eq_mk_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} : ⊤ = mk a ↔ a = 0

@[simp]

theorem MulArchimedeanClass.out_top (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : ⊤.out = 1

@[simp]

theorem ArchimedeanClass.out_top (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : ⊤.out = 0

instance MulArchimedeanClass.instNontrivial (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] [Nontrivial M] : Nontrivial (MulArchimedeanClass M)

instance ArchimedeanClass.instNontrivial (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Nontrivial M] : Nontrivial (ArchimedeanClass M)

theorem MulArchimedeanClass.mk_antitoneOn (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : AntitoneOn mk (Set.Ici 1)

theorem ArchimedeanClass.mk_antitoneOn (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : AntitoneOn mk (Set.Ici 0)

theorem MulArchimedeanClass.mk_monotoneOn (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : MonotoneOn mk (Set.Iic 1)

theorem ArchimedeanClass.mk_monotoneOn (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : MonotoneOn mk (Set.Iic 0)

theorem MulArchimedeanClass.min_le_mk_mul {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a b : M) : min (mk a) (mk b) ≤ mk (a * b)

theorem ArchimedeanClass.min_le_mk_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a b : M) : min (mk a) (mk b) ≤ mk (a + b)

theorem MulArchimedeanClass.mk_left_le_mk_mul {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (hab : mk a ≤ mk b) : mk a ≤ mk (a * b)

theorem ArchimedeanClass.mk_left_le_mk_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (hab : mk a ≤ mk b) : mk a ≤ mk (a + b)

theorem MulArchimedeanClass.mk_right_le_mk_mul {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (hba : mk b ≤ mk a) : mk b ≤ mk (a * b)

theorem ArchimedeanClass.mk_right_le_mk_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (hba : mk b ≤ mk a) : mk b ≤ mk (a + b)

theorem MulArchimedeanClass.mk_mul_eq_mk_left {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk a < mk b) : mk (a * b) = mk a

theorem ArchimedeanClass.mk_add_eq_mk_left {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk a < mk b) : mk (a + b) = mk a

theorem MulArchimedeanClass.mk_mul_eq_mk_right {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk b < mk a) : mk (a * b) = mk b

theorem ArchimedeanClass.mk_add_eq_mk_right {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk b < mk a) : mk (a + b) = mk b

theorem MulArchimedeanClass.mk_prod {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {ι : Type u_2} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hnonempty))

The product over a set of an elements in distinct classes is in the lowest class.

theorem ArchimedeanClass.mk_sum {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {ι : Type u_2} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} : StrictMonoOn (mk ∘ a) ↑s → mk (∑ i ∈ s, a i) = mk (a (s.min' hnonempty))

The sum over a set of an elements in distinct classes is in the lowest class.

theorem MulArchimedeanClass.lt_of_mk_lt_mk_of_one_le {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk a < mk b) (hpos : 1 ≤ a) : b < a

theorem ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk a < mk b) (hpos : 0 ≤ a) : b < a

theorem MulArchimedeanClass.lt_of_mk_lt_mk_of_le_one {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (h : mk a < mk b) (hneg : a ≤ 1) : a < b

theorem ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (h : mk a < mk b) (hneg : a ≤ 0) : a < b

theorem MulArchimedeanClass.one_lt_of_one_lt_of_mk_lt {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} (ha : 1 < a) (hab : mk a < mk (b / a)) : 1 < b

theorem ArchimedeanClass.pos_of_pos_of_mk_lt {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} (ha : 0 < a) (hab : mk a < mk (b - a)) : 0 < b

theorem MulArchimedeanClass.mulArchimedean_of_mk_eq_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b) : MulArchimedean M

theorem ArchimedeanClass.archimedean_of_mk_eq_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (h : ∀ (a : M), a ≠ 0 → ∀ (b : M), b ≠ 0 → mk a = mk b) : Archimedean M

theorem MulArchimedeanClass.mk_eq_mk_of_mulArchimedean {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} [MulArchimedean M] (ha : a ≠ 1) (hb : b ≠ 1) : mk a = mk b

theorem ArchimedeanClass.mk_eq_mk_of_archimedean {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} [Archimedean M] (ha : a ≠ 0) (hb : b ≠ 0) : mk a = mk b

noncomputable def MulArchimedeanClass.orderHom {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) : MulArchimedeanClass M →o MulArchimedeanClass N

An OrderMonoidHom can be lifted to an OrderHom over archimedean classes.

Equations

• MulArchimedeanClass.orderHom f = (MulArchimedeanOrder.orderHom f).antisymmetrization

noncomputable def ArchimedeanClass.orderHom {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) : ArchimedeanClass M →o ArchimedeanClass N

An OrderAddMonoidHom can be lifted to an OrderHom over archimedean classes.

Equations

• ArchimedeanClass.orderHom f = (ArchimedeanOrder.orderHom f).antisymmetrization

@[simp]

theorem MulArchimedeanClass.orderHom_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) (a : M) : (orderHom f) (mk a) = mk (f a)

@[simp]

theorem ArchimedeanClass.orderHom_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) (a : M) : (orderHom f) (mk a) = mk (f a)

theorem MulArchimedeanClass.map_mk_eq {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) (h : mk a = mk b) : mk (f a) = mk (f b)

theorem ArchimedeanClass.map_mk_eq {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) (h : mk a = mk b) : mk (f a) = mk (f b)

theorem MulArchimedeanClass.map_mk_le {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a b : M} {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) (h : mk a ≤ mk b) : mk (f a) ≤ mk (f b)

theorem ArchimedeanClass.map_mk_le {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a b : M} {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) (h : mk a ≤ mk b) : mk (f a) ≤ mk (f b)

theorem MulArchimedeanClass.orderHom_injective {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] {f : M →*o N} (h : Function.Injective ⇑f) : Function.Injective ⇑(orderHom f)

theorem ArchimedeanClass.orderHom_injective {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] {f : M →+o N} (h : Function.Injective ⇑f) : Function.Injective ⇑(orderHom f)

@[simp]

theorem MulArchimedeanClass.orderHom_top {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {N : Type u_2} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N] (f : M →*o N) : (orderHom f) ⊤ = ⊤

@[simp]

theorem ArchimedeanClass.orderHom_top {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {N : Type u_2} [AddCommGroup N] [LinearOrder N] [IsOrderedAddMonoid N] (f : M →+o N) : (orderHom f) ⊤ = ⊤

noncomputable def MulArchimedeanClass.liftOrderHom {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} [PartialOrder α] (f : M → α) (h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b) : MulArchimedeanClass M →o α

Lift a function M → α that's monotone along archimedean classes to a monotone function MulArchimedeanClass M →o α.

Equations

• MulArchimedeanClass.liftOrderHom f h = { toFun := MulArchimedeanClass.lift f ⋯, monotone' := ⋯ }

noncomputable def ArchimedeanClass.liftOrderHom {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} [PartialOrder α] (f : M → α) (h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b) : ArchimedeanClass M →o α

Lift a function M → α that's monotone along archimedean classes to a monotone function ArchimedeanClass M →o α.

Equations

• ArchimedeanClass.liftOrderHom f h = { toFun := ArchimedeanClass.lift f ⋯, monotone' := ⋯ }

@[simp]

theorem MulArchimedeanClass.liftOrderHom_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} [PartialOrder α] (f : M → α) (h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b) (a : M) : (liftOrderHom f h) (mk a) = f a

@[simp]

theorem ArchimedeanClass.liftOrderHom_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} [PartialOrder α] (f : M → α) (h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b) (a : M) : (liftOrderHom f h) (mk a) = f a

def MulArchimedeanClass.subsemigroup {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (s : UpperSet (MulArchimedeanClass M)) : Subsemigroup M

Given a UpperSet of MulArchimedeanClass, all group elements belonging to these classes form a subsemigroup. This is not yet a subgroup because it doesn't contain the identity if s = ⊤.

Equations

• MulArchimedeanClass.subsemigroup s = { carrier := MulArchimedeanClass.mk ⁻¹' ↑s, mul_mem' := ⋯ }

def ArchimedeanClass.subsemigroup {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (s : UpperSet (ArchimedeanClass M)) : AddSubsemigroup M

Given a UpperSet of ArchimedeanClass, all group elements belonging to these classes form a subsemigroup. This is not yet a subgroup because it doesn't contain the identity if s = ⊤.

Equations

• ArchimedeanClass.subsemigroup s = { carrier := ArchimedeanClass.mk ⁻¹' ↑s, add_mem' := ⋯ }

noncomputable def MulArchimedeanClass.subgroup {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (s : UpperSet (MulArchimedeanClass M)) : Subgroup M

Make MulArchimedeanClass.subsemigroup a subgroup by assigning s = ⊤ with a junk value ⊥.

Equations

• MulArchimedeanClass.subgroup s = if hs : s = ⊤ then ⊥ else let __src := MulArchimedeanClass.subsemigroup s; { toSubsemigroup := __src, one_mem' := ⋯, inv_mem' := ⋯ }

noncomputable def ArchimedeanClass.addSubgroup {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (s : UpperSet (ArchimedeanClass M)) : AddSubgroup M

Make ArchimedeanClass.subsemigroup a subgroup by assigning s = ⊤ with a junk value ⊥.

Equations

• ArchimedeanClass.addSubgroup s = if hs : s = ⊤ then ⊥ else let __src := ArchimedeanClass.subsemigroup s; { toAddSubsemigroup := __src, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem MulArchimedeanClass.subsemigroup_eq_subgroup_of_ne_top {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {s : UpperSet (MulArchimedeanClass M)} (hs : s ≠ ⊤) : ↑(subsemigroup s) = ↑(subgroup s)

theorem ArchimedeanClass.subsemigroup_eq_addSubgroup_of_ne_top {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {s : UpperSet (ArchimedeanClass M)} (hs : s ≠ ⊤) : ↑(subsemigroup s) = ↑(addSubgroup s)

@[simp]

theorem MulArchimedeanClass.subgroup_eq_bot (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : subgroup ⊤ = ⊥

@[simp]

theorem ArchimedeanClass.addSubgroup_eq_bot (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : addSubgroup ⊤ = ⊥

@[simp]

theorem MulArchimedeanClass.mem_subgroup_iff {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} {s : UpperSet (MulArchimedeanClass M)} (hs : s ≠ ⊤) : a ∈ subgroup s ↔ mk a ∈ s

@[simp]

theorem ArchimedeanClass.mem_addSubgroup_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} {s : UpperSet (ArchimedeanClass M)} (hs : s ≠ ⊤) : a ∈ addSubgroup s ↔ mk a ∈ s

theorem MulArchimedeanClass.subgroup_strictAntiOn {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : StrictAntiOn subgroup (Set.Iio ⊤)

theorem ArchimedeanClass.addSubgroup_strictAntiOn {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : StrictAntiOn addSubgroup (Set.Iio ⊤)

theorem MulArchimedeanClass.subgroup_antitone {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Antitone subgroup

theorem ArchimedeanClass.addSubgroup_antitone {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Antitone addSubgroup

@[reducible, inline]

noncomputable abbrev MulArchimedeanClass.ballSubgroup {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (c : MulArchimedeanClass M) : Subgroup M

An open ball defined by MulArchimedeanClass.subgroup of UpperSet.Ioi c. For c = ⊤, we assign the junk value ⊥.

Equations

• c.ballSubgroup = MulArchimedeanClass.subgroup (UpperSet.Ioi c)

@[reducible, inline]

noncomputable abbrev ArchimedeanClass.ballAddSubgroup {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (c : ArchimedeanClass M) : AddSubgroup M

An open ball defined by ArchimedeanClass.addSubgroup of UpperSet.Ioi c. For c = ⊤, we assign the junk value ⊥.

Equations

• c.ballAddSubgroup = ArchimedeanClass.addSubgroup (UpperSet.Ioi c)

@[reducible, inline]

noncomputable abbrev MulArchimedeanClass.closedBallSubgroup {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (c : MulArchimedeanClass M) : Subgroup M

A closed ball defined by MulArchimedeanClass.subgroup of UpperSet.Ici c.

Equations

• c.closedBallSubgroup = MulArchimedeanClass.subgroup (UpperSet.Ici c)

@[reducible, inline]

noncomputable abbrev ArchimedeanClass.closedBallAddSubgroup {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (c : ArchimedeanClass M) : AddSubgroup M

A closed ball defined by ArchimedeanClass.addSubgroup of UpperSet.Ici c.

Equations

• c.closedBallAddSubgroup = ArchimedeanClass.addSubgroup (UpperSet.Ici c)

theorem MulArchimedeanClass.mem_ballSubgroup_iff {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} {c : MulArchimedeanClass M} (hA : c ≠ ⊤) : a ∈ c.ballSubgroup ↔ c < mk a

theorem ArchimedeanClass.mem_ballAddSubgroup_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} {c : ArchimedeanClass M} (hA : c ≠ ⊤) : a ∈ c.ballAddSubgroup ↔ c < mk a

theorem MulArchimedeanClass.mem_closedBallSubgroup_iff {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} {c : MulArchimedeanClass M} : a ∈ c.closedBallSubgroup ↔ c ≤ mk a

theorem ArchimedeanClass.mem_closedBallAddSubgroup_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} {c : ArchimedeanClass M} : a ∈ c.closedBallAddSubgroup ↔ c ≤ mk a

@[simp]

theorem MulArchimedeanClass.ballSubgroup_top (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : ⊤.ballSubgroup = ⊥

@[simp]

theorem ArchimedeanClass.ballAddSubgroup_top (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : ⊤.ballAddSubgroup = ⊥

@[simp]

theorem MulArchimedeanClass.closedBallSubgroup_top (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : ⊤.closedBallSubgroup = ⊥

@[simp]

theorem ArchimedeanClass.closedBallAddSubgroup_top (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : ⊤.closedBallAddSubgroup = ⊥

theorem MulArchimedeanClass.ballSubgroup_antitone {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Antitone ballSubgroup

theorem ArchimedeanClass.ballAddSubgroup_antitone {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Antitone ballAddSubgroup

@[reducible, inline]

abbrev FiniteMulArchimedeanClass (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : Type u_1

FiniteMulArchimedeanClass M is the quotient of the non-one elements of the group M by multiplicative archimedean equivalence, where two elements a and b are in the same class iff (∃ m : ℕ, |b|ₘ ≤ |a|ₘ ^ m) ∧ (∃ n : ℕ, |a|ₘ ≤ |b|ₘ ^ n).

It is defined as the subtype of non-top elements of MulArchimedeanClass M (⊤ : MulArchimedeanClass M is the archimedean class of 1).

This is useful since the family of non-top archimedean classes is linearly independent.

Equations

• FiniteMulArchimedeanClass M = { A : MulArchimedeanClass M // A ≠ ⊤ }

@[reducible, inline]

abbrev FiniteArchimedeanClass (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : Type u_1

FiniteArchimedeanClass M is the quotient of the non-zero elements of the additive group M by additive archimedean equivalence, where two elements a and b are in the same class iff (∃ m : ℕ, |b| ≤ m • |a|) ∧ (∃ n : ℕ, |a| ≤ n • |b|).

It is defined as the subtype of non-top elements of ArchimedeanClass M (⊤ : ArchimedeanClass M is the archimedean class of 0).

This is useful since the family of non-top archimedean classes is linearly independent.

Equations

• FiniteArchimedeanClass M = { A : ArchimedeanClass M // A ≠ ⊤ }

def FiniteMulArchimedeanClass.mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (a : M) (h : a ≠ 1) : FiniteMulArchimedeanClass M

Create a FiniteMulArchimedeanClass from a non-one element.

Equations

• FiniteMulArchimedeanClass.mk a h = ⟨MulArchimedeanClass.mk a, ⋯⟩

def FiniteArchimedeanClass.mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (a : M) (h : a ≠ 0) : FiniteArchimedeanClass M

Create a FiniteArchimedeanClass from a non-zero element.

Equations

• FiniteArchimedeanClass.mk a h = ⟨ArchimedeanClass.mk a, ⋯⟩

@[simp]

theorem FiniteMulArchimedeanClass.val_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} (h : a ≠ 1) : ↑(mk a h) = MulArchimedeanClass.mk a

@[simp]

theorem FiniteArchimedeanClass.val_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} (h : a ≠ 0) : ↑(mk a h) = ArchimedeanClass.mk a

theorem FiniteMulArchimedeanClass.mk_le_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} (ha : a ≠ 1) {b : M} (hb : b ≠ 1) : mk a ha ≤ mk b hb ↔ MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b

theorem FiniteArchimedeanClass.mk_le_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} (ha : a ≠ 0) {b : M} (hb : b ≠ 0) : mk a ha ≤ mk b hb ↔ ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b

theorem FiniteMulArchimedeanClass.mk_lt_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} (ha : a ≠ 1) {b : M} (hb : b ≠ 1) : mk a ha < mk b hb ↔ MulArchimedeanClass.mk a < MulArchimedeanClass.mk b

theorem FiniteArchimedeanClass.mk_lt_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} (ha : a ≠ 0) {b : M} (hb : b ≠ 0) : mk a ha < mk b hb ↔ ArchimedeanClass.mk a < ArchimedeanClass.mk b

theorem FiniteMulArchimedeanClass.ind {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {motive : FiniteMulArchimedeanClass M → Prop} (mk : ∀ (a : M) (ha : a ≠ 1), motive (mk a ha)) (x : FiniteMulArchimedeanClass M) : motive x

An induction principle for FiniteMulArchimedeanClass.

theorem FiniteArchimedeanClass.ind {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {motive : FiniteArchimedeanClass M → Prop} (mk : ∀ (a : M) (ha : a ≠ 0), motive (mk a ha)) (x : FiniteArchimedeanClass M) : motive x

An induction principle for FiniteArchimedeanClass.

instance FiniteMulArchimedeanClass.instSubsingletonOfMulArchimedean {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] [MulArchimedean M] : Subsingleton (FiniteMulArchimedeanClass M)

instance FiniteArchimedeanClass.instSubsingletonOfAddArchimedean {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Archimedean M] : Subsingleton (FiniteArchimedeanClass M)

instance FiniteMulArchimedeanClass.instNonemptyOfNontrivial {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] [Nontrivial M] : Nonempty (FiniteMulArchimedeanClass M)

instance FiniteArchimedeanClass.instNonemptyOfNontrivial {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Nontrivial M] : Nonempty (FiniteArchimedeanClass M)

def FiniteMulArchimedeanClass.lift {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} (f : { a : M // a ≠ 1 } → α) (h : ∀ (a b : { a : M // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b) : FiniteMulArchimedeanClass M → α

Lift a f : {a : M // a ≠ 1} → α function to FiniteMulArchimedeanClass M → α.

Equations

• FiniteMulArchimedeanClass.lift f h ⟨A, hA⟩ = (MulArchimedeanClass.lift (fun (b : M) => if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A).untop ⋯

def FiniteArchimedeanClass.lift {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} (f : { a : M // a ≠ 0 } → α) (h : ∀ (a b : { a : M // a ≠ 0 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b) : FiniteArchimedeanClass M → α

Lift a f : {a : M // a ≠ 0} → α function to FiniteArchimedeanClass M → α.

Equations

• FiniteArchimedeanClass.lift f h ⟨A, hA⟩ = (ArchimedeanClass.lift (fun (b : M) => if h : b = 0 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A).untop ⋯

@[simp]

theorem FiniteMulArchimedeanClass.lift_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} (f : { a : M // a ≠ 1 } → α) (h : ∀ (a b : { a : M // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b) {a : M} (ha : a ≠ 1) : lift f h (mk a ha) = f ⟨a, ha⟩

@[simp]

theorem FiniteArchimedeanClass.lift_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} (f : { a : M // a ≠ 0 } → α) (h : ∀ (a b : { a : M // a ≠ 0 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b) {a : M} (ha : a ≠ 0) : lift f h (mk a ha) = f ⟨a, ha⟩

noncomputable def FiniteMulArchimedeanClass.liftOrderHom {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} [PartialOrder α] (f : { a : M // a ≠ 1 } → α) (h : ∀ (a b : { a : M // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b) : FiniteMulArchimedeanClass M →o α

Lift a function {a : M // a ≠ 1} → α that's monotone along archimedean classes to a monotone function FiniteMulArchimedeanClass M →o α.

Equations

• FiniteMulArchimedeanClass.liftOrderHom f h = { toFun := FiniteMulArchimedeanClass.lift f ⋯, monotone' := ⋯ }

noncomputable def FiniteArchimedeanClass.liftOrderHom {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} [PartialOrder α] (f : { a : M // a ≠ 0 } → α) (h : ∀ (a b : { a : M // a ≠ 0 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b) : FiniteArchimedeanClass M →o α

Lift a function {a : M // a ≠ 1} → α that's monotone along archimedean classes to a monotone function FiniteArchimedeanClass M₁ →o α.

Equations

• FiniteArchimedeanClass.liftOrderHom f h = { toFun := FiniteArchimedeanClass.lift f ⋯, monotone' := ⋯ }

@[simp]

theorem FiniteMulArchimedeanClass.liftOrderHom_mk {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {α : Type u_2} [PartialOrder α] (f : { a : M // a ≠ 1 } → α) (h : ∀ (a b : { a : M // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b) {a : M} (ha : a ≠ 1) : (liftOrderHom f h) (mk a ha) = f ⟨a, ha⟩

@[simp]

theorem FiniteArchimedeanClass.liftOrderHom_mk {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {α : Type u_2} [PartialOrder α] (f : { a : M // a ≠ 0 } → α) (h : ∀ (a b : { a : M // a ≠ 0 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b) {a : M} (ha : a ≠ 0) : (liftOrderHom f h) (mk a ha) = f ⟨a, ha⟩

noncomputable def FiniteMulArchimedeanClass.withTopOrderIso (M : Type u_1) [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] : WithTop (FiniteMulArchimedeanClass M) ≃o MulArchimedeanClass M

Adding top to the type of finite classes yields the type of all classes.

Equations

• FiniteMulArchimedeanClass.withTopOrderIso M = WithTop.subtypeOrderIso

noncomputable def FiniteArchimedeanClass.withTopOrderIso (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : WithTop (FiniteArchimedeanClass M) ≃o ArchimedeanClass M

Adding top to the type of finite classes yields the type of all classes.

Equations

• FiniteArchimedeanClass.withTopOrderIso M = WithTop.subtypeOrderIso

@[simp]

theorem FiniteMulArchimedeanClass.withTopOrderIso_apply_coe {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] (A : FiniteMulArchimedeanClass M) : (withTopOrderIso M) ↑A = ↑A

@[simp]

theorem FiniteArchimedeanClass.withTopOrderIso_apply_coe {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] (A : FiniteArchimedeanClass M) : (withTopOrderIso M) ↑A = ↑A

theorem FiniteMulArchimedeanClass.withTopOrderIso_symm_apply {M : Type u_1} [CommGroup M] [LinearOrder M] [IsOrderedMonoid M] {a : M} (h : a ≠ 1) : (withTopOrderIso M).symm (MulArchimedeanClass.mk a) = ↑(mk a h)

theorem FiniteArchimedeanClass.withTopOrderIso_symm_apply {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] {a : M} (h : a ≠ 0) : (withTopOrderIso M).symm (ArchimedeanClass.mk a) = ↑(mk a h)