Linearly ordered commutative additive groups and monoids with a top element adjoined

This file sets up a special class of linearly ordered commutative additive monoids that show up as the target of so-called “valuations” in algebraic number theory.

Usually, in the informal literature, these objects are constructed by taking a linearly ordered commutative additive group Γ and formally adjoining a top element: Γ ∪ {⊤}.

The disadvantage is that a type such as ENNReal is not of that form, whereas it is a very common target for valuations. The solutions is to use a typeclass, and that is exactly what we do in this file.

class LinearOrderedAddCommMonoidWithTop (α : Type u_3) extends AddCommMonoid α, LinearOrder α, IsOrderedAddMonoid α, OrderTop α : Type u_3

A linearly ordered commutative monoid with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : min a b = if a ≤ b then a else b
• max_def (a b : α) : max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• top : α
• le_top (a : α) : a ≤ ⊤
• top_add' (x : α) : ⊤ + x = ⊤

  In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is invariant under addition.

• isAddLeftRegular_of_ne_top ⦃x : α⦄ : x ≠ ⊤ → IsAddLeftRegular x

class LinearOrderedAddCommGroupWithTop (α : Type u_3) extends AddCommMonoid α, LinearOrder α, IsOrderedAddMonoid α, OrderTop α, SubNegMonoid α, Nontrivial α : Type u_3

A linearly ordered commutative group with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : min a b = if a ≤ b then a else b
• max_def (a b : α) : max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• top : α
• le_top (a : α) : a ≤ ⊤
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : LinearOrderedAddCommGroupWithTop.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : LinearOrderedAddCommGroupWithTop.zsmul (↑n.succ) a = LinearOrderedAddCommGroupWithTop.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : LinearOrderedAddCommGroupWithTop.zsmul (Int.negSucc n) a = -LinearOrderedAddCommGroupWithTop.zsmul (↑n.succ) a
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• top_add' (x : α) : ⊤ + x = ⊤

  In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is invariant under addition.

• neg_top : -⊤ = ⊤
• add_neg_cancel_of_ne_top ⦃x : α⦄ : x ≠ ⊤ → x + -x = 0

@[simp]

theorem top_add {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] (a : α) : ⊤ + a = ⊤

@[simp]

theorem add_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] (a : α) : a + ⊤ = ⊤

@[simp]

theorem IsAddRegular.of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a : α} (ha : a ≠ ⊤) : IsAddRegular a

theorem add_left_injective_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] (b : α) (h : b ≠ ⊤) : Function.Injective fun (x : α) => x + b

theorem add_right_injective_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] (b : α) (h : b ≠ ⊤) : Function.Injective fun (x : α) => b + x

@[simp]

theorem add_left_inj_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a b c : α} (h : a ≠ ⊤) : b + a = c + a ↔ b = c

@[simp]

theorem add_right_inj_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a b c : α} (h : a ≠ ⊤) : a + b = a + c ↔ b = c

theorem add_left_strictMono_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {b : α} (h : b ≠ ⊤) : StrictMono fun (x : α) => x + b

theorem add_right_strictMono_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {b : α} (h : b ≠ ⊤) : StrictMono fun (x : α) => b + x

@[simp]

theorem add_le_add_iff_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a b c : α} (h : a ≠ ⊤) : b + a ≤ c + a ↔ b ≤ c

@[simp]

theorem add_le_add_iff_right_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a b c : α} (h : a ≠ ⊤) : a + b ≤ a + c ↔ b ≤ c

@[simp]

theorem add_lt_add_iff_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a b c : α} (h : a ≠ ⊤) : b + a < c + a ↔ b < c

@[simp]

theorem add_lt_add_iff_right_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {a b c : α} (h : a ≠ ⊤) : a + b < a + c ↔ b < c

@[deprecated LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top (since := "2025-12-14")]

theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] ⦃x : α⦄ : x ≠ ⊤ → x + -x = 0

Alias of LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top.

Note: The following lemmas are special cases of the corresponding IsAddUnit lemmas.

theorem LinearOrderedAddCommGroupWithTop.neg_add_cancel_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} (ha : a ≠ ⊤) : -a + a = 0

theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} (ha : a ≠ ⊤) (b : α) : a + (-a + b) = b

theorem LinearOrderedAddCommGroupWithTop.neg_add_cancel_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} (ha : a ≠ ⊤) (b : α) : -a + (a + b) = b

theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_right_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {b : α} (hb : b ≠ ⊤) (a : α) : a + b + -b = a

theorem LinearOrderedAddCommGroupWithTop.neg_add_cancel_right_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {b : α} (hb : b ≠ ⊤) (a : α) : a + -b + b = a

@[simp]

theorem LinearOrderedAddCommGroupWithTop.top_ne_zero {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] : ⊤ ≠ 0

@[simp]

theorem LinearOrderedAddCommGroupWithTop.zero_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] : 0 ≠ ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.top_pos {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] : 0 < ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.isAddUnit_iff {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : IsAddUnit a ↔ a ≠ ⊤

instance LinearOrderedAddCommGroupWithTop.instLinearOrderedAddCommMonoidWithTop {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] : LinearOrderedAddCommMonoidWithTop α

theorem LinearOrderedAddCommGroupWithTop.add_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b : α} : a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.add_eq_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b : α} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.add_lt_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b : α} : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.neg_eq_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : -a = ⊤ ↔ a = ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : a - ⊤ = ⊤

@[instance 100]

instance LinearOrderedAddCommGroupWithTop.toSubtractionMonoid {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] : SubtractionMonoid α

@[deprecated add_left_injective_of_ne_top (since := "2025-12-27")]

theorem LinearOrderedAddCommGroupWithTop.injective_add_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] (b : α) (h : b ≠ ⊤) : Function.Injective fun (x : α) => x + b

Alias of add_left_injective_of_ne_top.

@[deprecated add_right_injective_of_ne_top (since := "2025-12-27")]

theorem LinearOrderedAddCommGroupWithTop.injective_add_right_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] (b : α) (h : b ≠ ⊤) : Function.Injective fun (x : α) => b + x

Alias of add_right_injective_of_ne_top.

theorem LinearOrderedAddCommGroupWithTop.sub_left_injective_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {b : α} (h : b ≠ ⊤) : Function.Injective fun (x : α) => x - b

theorem LinearOrderedAddCommGroupWithTop.sub_right_injective_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {b : α} (h : b ≠ ⊤) : Function.Injective fun (x : α) => b - x

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_left_inj_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b c : α} (h : a ≠ ⊤) : b - a = c - a ↔ b = c

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_right_inj_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b c : α} (h : a ≠ ⊤) : a - b = a - c ↔ b = c

@[deprecated add_left_strictMono_of_ne_top (since := "2025-12-27")]

theorem LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {b : α} (h : b ≠ ⊤) : StrictMono fun (x : α) => x + b

Alias of add_left_strictMono_of_ne_top.

@[deprecated add_right_strictMono_of_ne_top (since := "2025-12-27")]

theorem LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top {α : Type u_2} [LinearOrderedAddCommMonoidWithTop α] {b : α} (h : b ≠ ⊤) : StrictMono fun (x : α) => b + x

Alias of add_right_strictMono_of_ne_top.

theorem LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {b : α} (h : b ≠ ⊤) : StrictMono fun (x : α) => x - b

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_le_sub_iff_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b c : α} (h : a ≠ ⊤) : b - a ≤ c - a ↔ b ≤ c

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_lt_sub_iff_left_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b c : α} (h : a ≠ ⊤) : b - a < c - a ↔ b < c

@[simp]

theorem LinearOrderedAddCommGroupWithTop.add_neg_cancel_iff_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : a + -a = 0 ↔ a ≠ ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_iff_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : a - a = 0 ↔ a ≠ ⊤

theorem LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_of_ne_top {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : a ≠ ⊤ → a - a = 0

Alias of the reverse direction of LinearOrderedAddCommGroupWithTop.sub_self_eq_zero_iff_ne_top.

theorem LinearOrderedAddCommGroupWithTop.sub_pos {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b : α} : 0 < a - b ↔ b < a ∨ b = ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.neg_pos {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : 0 < -a ↔ a < 0 ∨ a = ⊤

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_self_nonneg {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a : α} : 0 ≤ a - a

@[simp]

theorem LinearOrderedAddCommGroupWithTop.sub_eq_zero {α : Type u_2} [LinearOrderedAddCommGroupWithTop α] {a b : α} (ha : a ≠ ⊤) : b - a = 0 ↔ b = a

instance WithTop.linearOrderedAddCommMonoidWithTop {α : Type u_2} [AddCancelCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] : LinearOrderedAddCommMonoidWithTop (WithTop α)

instance WithTop.LinearOrderedAddCommGroup.instNeg {G : Type u_1} [AddCommGroup G] : Neg (WithTop G)

instance WithTop.LinearOrderedAddCommGroup.instSub {G : Type u_1} [AddCommGroup G] : Sub (WithTop G)

If G has subtraction, we can extend the subtraction to WithTop G, by setting x - ⊤ = ⊤ and ⊤ - x = ⊤. This definition is only registered as an instance on additive commutative groups, to avoid conflicting with the instance WithTop.instSub on types with a bottom element.

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.coe_neg {G : Type u_1} [AddCommGroup G] (a : G) : ↑(-a) = -↑a

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.coe_sub {G : Type u_1} [AddCommGroup G] (a b : G) : ↑(a - b) = ↑a - ↑b

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.neg_top {G : Type u_1} [AddCommGroup G] : -⊤ = ⊤

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.top_sub {G : Type u_1} [AddCommGroup G] (x : WithTop G) : ⊤ - x = ⊤

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.sub_top {G : Type u_1} [AddCommGroup G] (x : WithTop G) : x - ⊤ = ⊤

@[simp]

theorem WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff {G : Type u_1} [AddCommGroup G] {x y : WithTop G} : x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤

instance WithTop.LinearOrderedAddCommGroup.instLinearOrderedAddCommGroupWithTopOfIsOrderedAddMonoid {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : LinearOrderedAddCommGroupWithTop (WithTop G)