mathlib3 documentation

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.

source
@[instance]
def linear_ordered_comm_group_with_zero.to_linear_ordered_comm_monoid_with_zero (α : Type u_1) [self : linear_ordered_comm_group_with_zero α] :
linear_ordered_comm_monoid_with_zero α
source
@[instance]
def linear_ordered_comm_group_with_zero.to_comm_group_with_zero (α : Type u_1) [self : 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

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
source
@[protected, 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 αᵒᵈ)
Equations
source
@[protected, instance]
def multiplicative.linear_ordered_comm_group_with_zero {α : Type u_1} [linear_ordered_add_comm_group_with_top α] :
linear_ordered_comm_group_with_zero (multiplicative αᵒᵈ)
Equations
source
@[protected, instance]
def with_zero.linear_ordered_comm_monoid_with_zero {α : Type u_1} [linear_ordered_comm_monoid α] :
linear_ordered_comm_monoid_with_zero (with_zero α)
Equations
source
@[protected, instance]
def with_zero.linear_ordered_comm_group_with_zero {α : Type u_1} [linear_ordered_comm_group α] :
linear_ordered_comm_group_with_zero (with_zero α)
Equations
source
@[reducible]
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 β] [has_pow β ℕ] [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)) :
linear_ordered_comm_monoid_with_zero β

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

Equations
source
@[simp]
theorem zero_le' {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
0 ≤ a
source
@[simp]
theorem not_lt_zero' {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
¬a < 0
source
@[simp]
theorem le_zero_iff {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
a ≤ 0 ↔ a = 0
source
theorem zero_lt_iff {α : Type u_1} {a : α} [linear_ordered_comm_monoid_with_zero α] :
0 < a ↔ a ≠ 0
source
theorem ne_zero_of_lt {α : Type u_1} {a b : α} [linear_ordered_comm_monoid_with_zero α] (h : b < a) :
a ≠ 0
source
@[protected, 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 αᵒᵈ)
Equations
source
theorem mul_le_one₀ {α : Type u_1} {a b : α} [linear_ordered_comm_group_with_zero α] (ha : a ≤ 1) (hb : b ≤ 1) :
a * b ≤ 1

Alias of mul_le_one' for unification.

source
theorem one_le_mul₀ {α : Type u_1} {a b : α} [linear_ordered_comm_group_with_zero α] (ha : 1 ≤ a) (hb : 1 ≤ b) :
1 ≤ a * b

Alias of one_le_mul' for unification.

source
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
source
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⁻¹
source
theorem mul_inv_le_of_le_mul {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (hab : a ≤ b * c) :
a * c⁻¹ ≤ b
source
theorem inv_le_one₀ {α : Type u_1} {a : α} [linear_ordered_comm_group_with_zero α] (ha : a ≠ 0) :
a⁻¹ ≤ 1 ↔ 1 ≤ a
source
theorem one_le_inv₀ {α : Type u_1} {a : α} [linear_ordered_comm_group_with_zero α] (ha : a ≠ 0) :
1 ≤ a⁻¹ ↔ a ≤ 1
source
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
source
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
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
@[simp]
theorem units.zero_lt {α : Type u_1} [linear_ordered_comm_group_with_zero α] (u : αˣ) :
0 < ↑u
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem mul_le_mul_left₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (ha : a ≠ 0) :
a * b ≤ a * c ↔ b ≤ c
source
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
source
theorem div_le_div_left₀ {α : Type u_1} {a b c : α} [linear_ordered_comm_group_with_zero α] (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) :
a / b ≤ a / c ↔ c ≤ b
source
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
source
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
source
@[simp]
theorem order_iso.mul_left₀'_apply {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} (ha : a ≠ 0) (ᾰ : α) :
⇑(order_iso.mul_left₀' ha) ᾰ = a * ᾰ
source
@[simp]
theorem order_iso.mul_left₀'_to_equiv {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} (ha : a ≠ 0) :
(order_iso.mul_left₀' ha).to_equiv = equiv.mul_left₀ a ha
source
def order_iso.mul_left₀' {α : Type u_1} [linear_ordered_comm_group_with_zero α] {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
source
theorem order_iso.mul_left₀'_symm {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} (ha : a ≠ 0) :
(order_iso.mul_left₀' ha).symm = order_iso.mul_left₀' _
source
@[simp]
theorem order_iso.mul_right₀'_apply {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} (ha : a ≠ 0) (ᾰ : α) :
⇑(order_iso.mul_right₀' ha) ᾰ = ᾰ * a
source
def order_iso.mul_right₀' {α : Type u_1} [linear_ordered_comm_group_with_zero α] {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
source
@[simp]
theorem order_iso.mul_right₀'_to_equiv {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} (ha : a ≠ 0) :
(order_iso.mul_right₀' ha).to_equiv = equiv.mul_right₀ a ha
source
theorem order_iso.mul_right₀'_symm {α : Type u_1} [linear_ordered_comm_group_with_zero α] {a : α} (ha : a ≠ 0) :
(order_iso.mul_right₀' ha).symm = order_iso.mul_right₀' _
source
@[protected, instance]
def additive.linear_ordered_add_comm_group_with_top {α : Type u_1} [linear_ordered_comm_group_with_zero α] :
linear_ordered_add_comm_group_with_top (additive αᵒᵈ)
Equations