mathlib documentation

algebra.linear_ordered_comm_group_with_zero

Linearly ordered commutative groups 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.

source
@[instance]
def linear_ordered_comm_group_with_zero.to_linear_order (α : Type u_1) [s : linear_ordered_comm_group_with_zero α] :
linear_order α

source
@[instance]
def linear_ordered_comm_group_with_zero.to_comm_group_with_zero (α : Type u_1) [s : linear_ordered_comm_group_with_zero α] :
comm_group_with_zero α

source
@[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 ≤ b → b ≤ c_1 → a ≤ c_1
  • 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
  • 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
  • inv : α → α
  • exists_pair_ne : ∃ (x y : α), x ≠ y
  • inv_zero : 0⁻¹ = 0
  • mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
  • mul_le_mul_left : ∀ {a b : α}, a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
  • zero_le_one : 0 ≤ 1

A linearly ordered commutative group with a zero element.

Instances
source
@[instance]
def linear_ordered_comm_group_with_zero.to_ordered_comm_monoid {α : Type u_1} [linear_ordered_comm_group_with_zero α] :
ordered_comm_monoid α

Every linearly ordered commutative group with zero is an ordered commutative monoid.

Equations
source
theorem one_le_pow_of_one_le' {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : ℕ} (H : 1 ≤ x) :
1 ≤ x ^ n

source
theorem pow_le_one_of_le_one {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : ℕ} (H : x ≤ 1) :
x ^ n ≤ 1

source
theorem eq_one_of_pow_eq_one {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : ℕ} (hn : n ≠ 0) (H : x ^ n = 1) :
x = 1

source
theorem pow_eq_one_iff {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : ℕ} (hn : n ≠ 0) :
x ^ n = 1 ↔ x = 1

source
theorem one_le_pow_iff {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : ℕ} (hn : n ≠ 0) :
1 ≤ x ^ n ↔ 1 ≤ x

source
theorem pow_le_one_iff {α : Type u_1} [linear_ordered_comm_group_with_zero α] {x : α} {n : ℕ} (hn : n ≠ 0) :
x ^ n ≤ 1 ↔ x ≤ 1

source
theorem zero_le_one' {α : Type u_1} [linear_ordered_comm_group_with_zero α] :
0 ≤ 1

source
theorem zero_lt_one' {α : Type u_1} [linear_ordered_comm_group_with_zero α] :
0 < 1

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

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

source
@[simp]
theorem le_zero_iff {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} :
a ≤ 0 ↔ a = 0

source
theorem zero_lt_iff {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} :
0 < a ↔ a ≠ 0

source
theorem le_of_le_mul_right {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b c : α} (h : c ≠ 0) (hab : a * c ≤ b * c) :
a ≤ b

source
theorem le_mul_inv_of_mul_le {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b c : α} (h : c ≠ 0) (hab : a * c ≤ b) :
a ≤ b * c⁻¹

source
theorem mul_inv_le_of_le_mul {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b c : α} (h : c ≠ 0) (hab : a ≤ b * c) :
a * c⁻¹ ≤ b

source
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

source
theorem ne_zero_of_lt {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b : α} (h : b < a) :
a ≠ 0

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

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

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

source
theorem mul_lt_right' {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b : α} (c : α) (h : a < b) (hc : c ≠ 0) :
a * c < b * c

source
theorem inv_lt_inv'' {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
a⁻¹ < b⁻¹ ↔ b < a

source
theorem inv_le_inv'' {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
a⁻¹ ≤ b⁻¹ ↔ b ≤ a