mathlib documentation

algebra.order.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.

@[class]
structure linear_ordered_comm_group_with_zero (α : Type u_1) :
Type u_1

A linearly ordered commutative group with a zero element.

Instances
@[protected, instance]
Equations
@[protected, instance]
Equations
def function.injective.linear_ordered_comm_monoid_with_zero {α : Type u_1} [linear_ordered_comm_monoid_with_zero α] {β : Type u_2} [has_zero β] [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

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

Equations
theorem zero_le_one' {α : Type u_1} [linear_ordered_comm_monoid_with_zero α] :
0 1
@[simp]
theorem zero_le' {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
0 a
@[simp]
theorem not_lt_zero' {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
¬a < 0
@[simp]
theorem le_zero_iff {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
a 0 a = 0
theorem zero_lt_iff {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
0 < a a 0
theorem ne_zero_of_lt {α : Type u_1} {a b : α} [linear_ordered_comm_monoid_with_zero α] (h : b < a) :
a 0
theorem pow_pos_iff {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] [no_zero_divisors α] {n : } (hn : 0 < n) :
0 < a ^ n 0 < a
theorem zero_lt_one₀ {α : Type u_1} [linear_ordered_comm_group_with_zero α] :
0 < 1
theorem le_of_le_mul_right {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (h : c 0) (hab : a * c b * c) :
a b
theorem le_mul_inv_of_mul_le {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (h : c 0) (hab : a * c b) :
a b * c⁻¹
theorem mul_inv_le_of_le_mul {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (h : c 0) (hab : a b * c) :
a * c⁻¹ b
theorem le_mul_inv_iff₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hc : c 0) :
a b * c⁻¹ a * c b
theorem mul_inv_le_iff₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hc : c 0) :
a * c⁻¹ b a b * c
theorem div_le_div₀ {α : Type u_1} [linear_ordered_comm_group_with_zero α] (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} [linear_ordered_comm_group_with_zero α] (u : units α) :
0 < u
theorem mul_lt_mul_of_lt_of_le₀ {α : Type u_1} {a b c d : α} [linear_ordered_comm_group_with_zero α] (hab : a b) (hb : b 0) (hcd : c < d) :
a * c < b * d
theorem mul_lt_mul₀ {α : Type u_1} {a b c d : α} [linear_ordered_comm_group_with_zero α] (hab : a < b) (hcd : c < d) :
a * c < b * d
theorem mul_inv_lt_of_lt_mul₀ {α : Type u_1} {x y z : α} [linear_ordered_comm_group_with_zero α] (h : x < y * z) :
x * z⁻¹ < y
theorem inv_mul_lt_of_lt_mul₀ {α : Type u_1} {x y z : α} [linear_ordered_comm_group_with_zero α] (h : x < y * z) :
y⁻¹ * x < z
theorem mul_lt_right₀ {α : Type u_1} {a b : α} [linear_ordered_comm_group_with_zero α] (c : α) (h : a < b) (hc : c 0) :
a * c < b * c
theorem pow_lt_pow_succ {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : } (hx : 1 < x) :
x ^ n < x ^ n.succ
theorem pow_lt_pow₀ {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {m n : } (hx : 1 < x) (hmn : m < n) :
x ^ m < x ^ n
theorem inv_lt_inv₀ {α : Type u_1} {a b : α} [linear_ordered_comm_group_with_zero α] (ha : a 0) (hb : b 0) :
a⁻¹ < b⁻¹ b < a
theorem inv_le_inv₀ {α : Type u_1} {a b : α} [linear_ordered_comm_group_with_zero α] (ha : a 0) (hb : b 0) :
theorem lt_of_mul_lt_mul_of_le₀ {α : Type u_1} {a b c d : α} [linear_ordered_comm_group_with_zero α] (h : a * b < c * d) (hc : 0 < c) (hh : c a) :
b < d
theorem mul_le_mul_right₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hc : c 0) :
a * c b * c a b
theorem div_le_div_right₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hc : c 0) :
a / c b / c a b
theorem le_div_iff₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hc : c 0) :
a b / c a * c b
theorem div_le_iff₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hc : c 0) :
a / c b a b * c
@[protected, instance]
Equations
theorem monoid_hom.map_neg_one {α : Type u_1} [linear_ordered_comm_group_with_zero α] {R : Type u_2} [ring R] (f : R →* α) :
f (-1) = 1
@[simp]
theorem monoid_hom.map_neg {α : Type u_1} [linear_ordered_comm_group_with_zero α] {R : Type u_2} [ring R] (f : R →* α) (x : R) :
f (-x) = f x
theorem monoid_hom.map_sub_swap {α : Type u_1} [linear_ordered_comm_group_with_zero α] {R : Type u_2} [ring R] (f : R →* α) (x y : R) :
f (x - y) = f (y - x)