# mathlibdocumentation

algebra.linear_ordered_comm_group_with_zero

# Linearly ordered commutative groups and monoids with a zero element adjoined

This file sets up a special class of linearly ordered commutative 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 group Γ and formally adjoining a zero element: Γ ∪ {0}.

The disadvantage is that a type such as nnreal 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.

Note that to avoid issues with import cycles, linear_ordered_comm_monoid_with_zero is defined in another file. However, the lemmas about it are stated here.

@[instance]

@[instance]

@[class]
structure linear_ordered_comm_group_with_zero (α : Type u_1) :
Type u_1
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
• lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• mul_comm : ∀ (a b : α), a * b = b * a
• zero : α
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_le_mul_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 * a c_1 * b
• lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1b < c_1
• zero_le_one : 0 1
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• exists_pair_ne : ∃ (x y : α), x y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

A linearly ordered commutative group with a zero element.

Instances
theorem one_le_pow_of_one_le' {α : Type u_1} {x : α} {n : } (H : 1 x) :
1 x ^ n

theorem pow_le_one_of_le_one {α : Type u_1} {x : α} {n : } (H : x 1) :
x ^ n 1

theorem eq_one_of_pow_eq_one {α : Type u_1} {x : α} {n : } (hn : n 0) (H : x ^ n = 1) :
x = 1

theorem pow_eq_one_iff {α : Type u_1} {x : α} {n : } (hn : n 0) :
x ^ n = 1 x = 1

theorem one_le_pow_iff {α : Type u_1} {x : α} {n : } (hn : n 0) :
1 x ^ n 1 x

theorem pow_le_one_iff {α : Type u_1} {x : α} {n : } (hn : n 0) :
x ^ n 1 x 1

theorem zero_le_one' {α : Type u_1}  :
0 1

@[simp]
theorem zero_le' {α : Type u_1} {a : α}  :
0 a

@[simp]
theorem not_lt_zero' {α : Type u_1} {a : α}  :
¬a < 0

@[simp]
theorem le_zero_iff {α : Type u_1} {a : α}  :
a 0 a = 0

theorem zero_lt_iff {α : Type u_1} {a : α}  :
0 < a a 0

theorem ne_zero_of_lt {α : Type u_1} {a b : α} (h : b < a) :
a 0

theorem zero_lt_one'' {α : Type u_1}  :
0 < 1

theorem le_of_le_mul_right {α : Type u_1} {a b c : α} (h : c 0) (hab : a * c b * c) :
a b

theorem le_mul_inv_of_mul_le {α : Type u_1} {a b c : α} (h : c 0) (hab : a * c b) :
a b * c⁻¹

theorem mul_inv_le_of_le_mul {α : Type u_1} {a b c : α} (h : c 0) (hab : a b * c) :
a * c⁻¹ b

theorem div_le_div' {α : Type u_1} (a b c d : α) (hb : b 0) (hd : d 0) :
a * b⁻¹ c * d⁻¹ a * d c * b

@[simp]
theorem units.zero_lt {α : Type u_1} (u : units α) :
0 < u

theorem mul_lt_mul'''' {α : Type u_1} {a b c d : α} (hab : a < b) (hcd : c < d) :
a * c < b * d

theorem mul_inv_lt_of_lt_mul' {α : Type u_1} {x y z : α} (h : x < y * z) :
x * z⁻¹ < y

theorem mul_lt_right' {α : Type u_1} {a b : α} (c : α) (h : a < b) (hc : c 0) :
a * c < b * c

theorem pow_lt_pow_succ {α : Type u_1} {x : α} {n : } (hx : 1 < x) :
x ^ n < x ^ n.succ

theorem pow_lt_pow' {α : Type u_1} {x : α} {m n : } (hx : 1 < x) (hmn : m < n) :
x ^ m < x ^ n

theorem inv_lt_inv'' {α : Type u_1} {a b : α} (ha : a 0) (hb : b 0) :
a⁻¹ < b⁻¹ b < a

theorem inv_le_inv'' {α : Type u_1} {a b : α} (ha : a 0) (hb : b 0) :

theorem monoid_hom.map_neg_one {α : Type u_1} {R : Type u_2} [ring R] (f : R →* α) :
f (-1) = 1

@[simp]
theorem monoid_hom.map_neg {α : Type u_1} {R : Type u_2} [ring R] (f : R →* α) (x : R) :
f (-x) = f x

theorem monoid_hom.map_sub_swap {α : Type u_1} {R : Type u_2} [ring R] (f : R →* α) (x y : R) :
f (x - y) = f (y - x)