mathlib documentation

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]

def linear_ordered_comm_group_with_zero.to_linear_ordered_comm_monoid_with_zero (α : Type u_1) [s : linear_ordered_comm_group_with_zero α] :

linear_ordered_comm_monoid_with_zero α

@[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 α

@[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
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.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
npow : ℕ → α → α
npow_zero' : (∀ (x : α), linear_ordered_comm_group_with_zero.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_comm_group_with_zero.npow n.succ x = x * linear_ordered_comm_group_with_zero.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a
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_1 → b < c_1
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"
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

@[instance]

def multiplicative.linear_ordered_comm_monoid_with_zero {α : Type u_1} [linear_ordered_add_comm_monoid_with_top α] :

linear_ordered_comm_monoid_with_zero (multiplicative (order_dual α))

Equations

multiplicative.linear_ordered_comm_monoid_with_zero = {le := ordered_comm_monoid.le multiplicative.ordered_comm_monoid, lt := ordered_comm_monoid.lt multiplicative.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le multiplicative.linear_order, decidable_eq := linear_order.decidable_eq multiplicative.linear_order, decidable_lt := linear_order.decidable_lt multiplicative.linear_order, mul := ordered_comm_monoid.mul multiplicative.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one multiplicative.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow multiplicative.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _, zero := ⇑multiplicative.of_add ⊤, zero_mul := _, mul_zero := _, zero_le_one := _}

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) :

linear_ordered_comm_monoid_with_zero β

Pullback a linear_ordered_comm_monoid_with_zero under an injective map.

Equations

function.injective.linear_ordered_comm_monoid_with_zero f hf zero one mul = {le := linear_order.le (linear_order.lift f hf), lt := linear_order.lt (linear_order.lift f hf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift f hf), decidable_eq := linear_order.decidable_eq (linear_order.lift f hf), decidable_lt := linear_order.decidable_lt (linear_order.lift f hf), mul := ordered_comm_monoid.mul (function.injective.ordered_comm_monoid f hf one mul), mul_assoc := _, one := ordered_comm_monoid.one (function.injective.ordered_comm_monoid f hf one mul), one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow (function.injective.ordered_comm_monoid f hf one mul), npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _, zero := comm_monoid_with_zero.zero (function.injective.comm_monoid_with_zero f hf zero one mul), zero_mul := _, mul_zero := _, zero_le_one := _}

theorem one_le_pow_of_one_le' {α : Type u_1} {x : α} [linear_ordered_comm_monoid_with_zero α] {n : ℕ} (H : 1 ≤ x) :

1 ≤ x ^ n

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

x ^ n ≤ 1

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

x = 1

theorem pow_eq_one_iff {α : Type u_1} {x : α} [linear_ordered_comm_monoid_with_zero α] {n : ℕ} (hn : n ≠ 0) :

x ^ n = 1 ↔ x = 1

theorem one_le_pow_iff {α : Type u_1} {x : α} [linear_ordered_comm_monoid_with_zero α] {n : ℕ} (hn : n ≠ 0) :

1 ≤ x ^ n ↔ 1 ≤ x

theorem pow_le_one_iff {α : Type u_1} {x : α} [linear_ordered_comm_monoid_with_zero α] {n : ℕ} (hn : n ≠ 0) :

x ^ n ≤ 1 ↔ x ≤ 1

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

@[instance]

def additive.linear_ordered_add_comm_monoid_with_top {α : Type u_1} [linear_ordered_comm_monoid_with_zero α] :

linear_ordered_add_comm_monoid_with_top (additive (order_dual α))

Equations

additive.linear_ordered_add_comm_monoid_with_top = {le := ordered_add_comm_monoid.le additive.ordered_add_comm_monoid, lt := ordered_add_comm_monoid.lt additive.ordered_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le additive.linear_order, decidable_eq := linear_order.decidable_eq additive.linear_order, decidable_lt := linear_order.decidable_lt additive.linear_order, add := ordered_add_comm_monoid.add additive.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero additive.ordered_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_add_comm_monoid.nsmul additive.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, top := 0, le_top := _, top_add' := _}

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 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'''' {α : 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 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) :

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

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)