# mathlib3documentation

algebra.order.with_zero

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α), a b b c a c
• lt_iff_le_not_le : ( (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : (a b : α), a b b a a = b
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"
• mul : α α α
• mul_assoc : (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : (a : α), 1 * a = a
• mul_one : (a : α), a * 1 = a
• npow : α α
• npow_zero' : ( (x : α), . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), . "try_refl_tac"
• mul_comm : (a b : α), a * b = b * a
• mul_le_mul_left : (a b : α), a b (c : α), c * a c * b
• zero : α
• zero_mul : (a : α), 0 * a = 0
• mul_zero : (a : α), a * 0 = 0
• zero_le_one : 0 1
• inv : α α
• div : α α α
• div_eq_mul_inv : ( (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : α α
• zpow_zero' : ( (a : α), . "try_refl_tac"
• zpow_succ' : ( (n : ) (a : α), . "try_refl_tac"
• zpow_neg' : ( (n : ) (a : α), . "try_refl_tac"
• exists_pair_ne : (x y : α), x y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : (a : α), a 0 a * a⁻¹ = 1

A linearly ordered commutative group with a zero element.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_group_with_zero
• linear_ordered_comm_group_with_zero.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
@[reducible]
def function.injective.linear_ordered_comm_monoid_with_zero {α : Type u_1} {β : Type u_2} [has_zero β] [has_one β] [has_mul β] [ ] [has_sup β] [has_inf β] (f : β α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : (x y : β), f (x * y) = f x * f y) (npow : (x : β) (n : ), f (x ^ n) = f x ^ n) (hsup : (x y : β), f (x y) = linear_order.max (f x) (f y)) (hinf : (x y : β), f (x y) = linear_order.min (f x) (f y)) :

Pullback a linear_ordered_comm_monoid_with_zero under an injective map. See note [reducible non-instances].

Equations
@[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
@[protected, instance]
Equations
theorem mul_le_one₀ {α : Type u_1} {a b : α} (ha : a 1) (hb : b 1) :
a * b 1

Alias of mul_le_one' for unification.

theorem one_le_mul₀ {α : Type u_1} {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b

Alias of one_le_mul' for unification.

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 : α} (hab : a b * c) :
a * c⁻¹ b
theorem inv_le_one₀ {α : Type u_1} {a : α} (ha : a 0) :
a⁻¹ 1 1 a
theorem one_le_inv₀ {α : Type u_1} {a : α} (ha : a 0) :
1 a⁻¹ a 1
theorem le_mul_inv_iff₀ {α : Type u_1} {a b c : α} (hc : c 0) :
a b * c⁻¹ a * c b
theorem mul_inv_le_iff₀ {α : Type u_1} {a b c : α} (hc : c 0) :
a * c⁻¹ b a b * c
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 : αˣ) :
0 < u
theorem mul_lt_mul_of_lt_of_le₀ {α : Type u_1} {a b c d : α} (hab : a b) (hb : b 0) (hcd : c < d) :
a * c < b * d
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 inv_mul_lt_of_lt_mul₀ {α : Type u_1} {x y z : α} (h : x < y * z) :
y⁻¹ * x < z
theorem mul_lt_right₀ {α : Type u_1} {a b : α} (c : α) (h : a < b) (hc : c 0) :
a * c < b * c
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 lt_of_mul_lt_mul_of_le₀ {α : Type u_1} {a b c d : α} (h : a * b < c * d) (hc : 0 < c) (hh : c a) :
b < d
theorem mul_le_mul_right₀ {α : Type u_1} {a b c : α} (hc : c 0) :
a * c b * c a b
theorem mul_le_mul_left₀ {α : Type u_1} {a b c : α} (ha : a 0) :
a * b a * c b c
theorem div_le_div_right₀ {α : Type u_1} {a b c : α} (hc : c 0) :
a / c b / c a b
theorem div_le_div_left₀ {α : Type u_1} {a b c : α} (ha : a 0) (hb : b 0) (hc : c 0) :
a / b a / c c b
theorem le_div_iff₀ {α : Type u_1} {a b c : α} (hc : c 0) :
a b / c a * c b
theorem div_le_iff₀ {α : Type u_1} {a b c : α} (hc : c 0) :
a / c b a b * c
@[simp]
theorem order_iso.mul_left₀'_apply {α : Type u_1} {a : α} (ha : a 0) (ᾰ : α) :
= a *
@[simp]
theorem order_iso.mul_left₀'_to_equiv {α : Type u_1} {a : α} (ha : a 0) :
= ha
def order_iso.mul_left₀' {α : Type u_1} {a : α} (ha : a 0) :
α ≃o α

equiv.mul_left₀ as an order_iso on a linear_ordered_comm_group_with_zero..

Note that order_iso.mul_left₀ refers to the linear_ordered_field version.

Equations
theorem order_iso.mul_left₀'_symm {α : Type u_1} {a : α} (ha : a 0) :
@[simp]
theorem order_iso.mul_right₀'_apply {α : Type u_1} {a : α} (ha : a 0) (ᾰ : α) :
= * a
def order_iso.mul_right₀' {α : Type u_1} {a : α} (ha : a 0) :
α ≃o α

equiv.mul_right₀ as an order_iso on a linear_ordered_comm_group_with_zero..

Note that order_iso.mul_right₀ refers to the linear_ordered_field version.

Equations
@[simp]
theorem order_iso.mul_right₀'_to_equiv {α : Type u_1} {a : α} (ha : a 0) :
theorem order_iso.mul_right₀'_symm {α : Type u_1} {a : α} (ha : a 0) :