# 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.

class LinearOrderedCommMonoidWithZero (α : Type u_2) extends , :
Type u_2

A linearly ordered commutative monoid with a zero element.

• 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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun (x x_1 : α) => x x_1
• decidableEq :
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• 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 =
• zero : α
• zero_mul : ∀ (a : α), 0 * a = 0

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : α), a * 0 = 0

Zero is a right absorbing element for multiplication

• zero_le_one : 0 1

0 ≤ 1 in any linearly ordered commutative monoid.

Instances
theorem LinearOrderedCommMonoidWithZero.zero_le_one {α : Type u_2} [self : ] :
0 1

0 ≤ 1 in any linearly ordered commutative monoid.

class LinearOrderedCommGroupWithZero (α : Type u_2) extends , , , :
Type u_2

A linearly ordered commutative group with a zero element.

• 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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun (x x_1 : α) => x x_1
• decidableEq :
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• 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 =
• 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⁻¹

a / b := a * b⁻¹

• zpow : αα

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α),

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : α),

a ^ (n + 1) = a ^ n * a

• zpow_neg' : ∀ (n : ) (a : α), = (LinearOrderedCommGroupWithZero.zpow (n.succ) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
• inv_zero : 0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

Instances
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[reducible, inline]
abbrev Function.Injective.linearOrderedCommMonoidWithZero {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Mul β] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : ) (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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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
Equations
theorem pow_pos_iff {α : Type u_1} {a : α} {n : } [] (hn : n 0) :
0 < a ^ n 0 < a
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} {a : α} {b : α} {c : α} (h : a < b * c) :
a * c⁻¹ < b
theorem inv_mul_lt_of_lt_mul₀ {α : Type u_1} {a : α} {b : α} {c : α} (h : a < b * c) :
b⁻¹ * a < c
theorem mul_lt_right₀ {α : Type u_1} {a : α} {b : α} (c : α) (h : a < b) (hc : c 0) :
a * c < b * c
theorem inv_lt_one₀ {α : Type u_1} {a : α} (ha : a 0) :
a⁻¹ < 1 1 < a
theorem one_lt_inv₀ {α : Type u_1} {a : α} (ha : a 0) :
1 < a⁻¹ a < 1
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 OrderIso.mulLeft₀'_apply {α : Type u_1} {a : α} (ha : a 0) (x : α) :
() x = a * x
@[simp]
theorem OrderIso.mulLeft₀'_toEquiv {α : Type u_1} {a : α} (ha : a 0) :
().toEquiv =
def OrderIso.mulLeft₀' {α : Type u_1} {a : α} (ha : a 0) :
α ≃o α

Equiv.mulLeft₀ as an OrderIso on a LinearOrderedCommGroupWithZero..

Note that OrderIso.mulLeft₀ refers to the LinearOrderedField version.

Equations
• = let __src := ; { toEquiv := __src, map_rel_iff' := }
Instances For
theorem OrderIso.mulLeft₀'_symm {α : Type u_1} {a : α} (ha : a 0) :
().symm =
@[simp]
theorem OrderIso.mulRight₀'_apply {α : Type u_1} {a : α} (ha : a 0) (x : α) :
() x = x * a
@[simp]
theorem OrderIso.mulRight₀'_toEquiv {α : Type u_1} {a : α} (ha : a 0) :
().toEquiv =
def OrderIso.mulRight₀' {α : Type u_1} {a : α} (ha : a 0) :
α ≃o α

Equiv.mulRight₀ as an OrderIso on a LinearOrderedCommGroupWithZero..

Note that OrderIso.mulRight₀ refers to the LinearOrderedField version.

Equations
• = let __src := ; { toEquiv := __src, map_rel_iff' := }
Instances For
theorem OrderIso.mulRight₀'_symm {α : Type u_1} {a : α} (ha : a 0) :
().symm =
Equations
• One or more equations did not get rendered due to their size.
theorem pow_lt_pow_succ {α : Type u_1} {a : α} {n : } (ha : 1 < a) :
a ^ n < a ^ n.succ
theorem pow_lt_pow_right₀ {α : Type u_1} {a : α} {m : } {n : } (ha : 1 < a) (hmn : m < n) :
a ^ m < a ^ n
@[deprecated pow_lt_pow_right₀]
theorem pow_lt_pow₀ {α : Type u_1} {a : α} {m : } {n : } (ha : 1 < a) (hmn : m < n) :
a ^ m < a ^ n

Alias of pow_lt_pow_right₀.

Equations
• instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual = let __src := Multiplicative.orderedCommMonoid; let __src_1 := Multiplicative.linearOrder;
Equations
• One or more equations did not get rendered due to their size.
instance WithZero.preorder {α : Type u_1} [] :
Equations
• WithZero.preorder = WithBot.preorder
instance WithZero.orderBot {α : Type u_1} [] :
Equations
• WithZero.orderBot = WithBot.orderBot
theorem WithZero.zero_le {α : Type u_1} [] (a : ) :
0 a
theorem WithZero.zero_lt_coe {α : Type u_1} [] (a : α) :
0 < a
theorem WithZero.zero_eq_bot {α : Type u_1} [] :
0 =
@[simp]
theorem WithZero.coe_lt_coe {α : Type u_1} [] {a : α} {b : α} :
a < b a < b
@[simp]
theorem WithZero.coe_le_coe {α : Type u_1} [] {a : α} {b : α} :
a b a b
theorem WithZero.coe_le_iff {α : Type u_1} [] {a : α} {x : } :
a x ∃ (b : α), x = b a b
instance WithZero.covariantClass_mul_le {α : Type u_1} [] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :
CovariantClass () () (fun (x x_1 : ) => x * x_1) fun (x x_1 : ) => x x_1
Equations
• =
theorem WithZero.covariantClass_add_le {α : Type u_1} [] [] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (h : ∀ (a : α), 0 a) :
CovariantClass () () (fun (x x_1 : ) => x + x_1) fun (x x_1 : ) => x x_1
instance WithZero.existsAddOfLE {α : Type u_1} [] [Add α] [] :
Equations
• =
instance WithZero.partialOrder {α : Type u_1} [] :
Equations
• WithZero.partialOrder = WithBot.partialOrder
instance WithZero.contravariantClass_mul_lt {α : Type u_1} [] [Mul α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] :
ContravariantClass () () (fun (x x_1 : ) => x * x_1) fun (x x_1 : ) => x < x_1
Equations
• =
instance WithZero.lattice {α : Type u_1} [] :
Equations
• WithZero.lattice = WithBot.lattice
instance WithZero.linearOrder {α : Type u_1} [] :
Equations
• WithZero.linearOrder = WithBot.linearOrder
theorem WithZero.le_max_iff {α : Type u_1} [] {a : α} {b : α} {c : α} :
a max b c a max b c
theorem WithZero.min_le_iff {α : Type u_1} [] {a : α} {b : α} {c : α} :
min a b c min a b c
instance WithZero.orderedCommMonoid {α : Type u_1} :
Equations
• WithZero.orderedCommMonoid = let __src := CommMonoidWithZero.toCommMonoid; let __src_1 := WithZero.partialOrder;
@[reducible, inline]
abbrev WithZero.orderedAddCommMonoid {α : Type u_1} (zero_le : ∀ (a : α), 0 a) :

If 0 is the least element in α, then WithZero α is an OrderedAddCommMonoid.

Equations
• = let __src := WithZero.partialOrder; let __src_1 := WithZero.addCommMonoid;
Instances For

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations
• WithZero.canonicallyOrderedAddCommMonoid = let __src := WithZero.orderBot; let __src_1 := ; let __src_2 := ;
Equations
• One or more equations did not get rendered due to their size.
Equations
• WithZero.instLinearOrderedCommMonoidWithZero = let __src := WithZero.linearOrder; let __src_1 := WithZero.commMonoidWithZero;
Equations
• One or more equations did not get rendered due to their size.