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.
@[class]
- 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.
@[instance]
def
linear_ordered_comm_group_with_zero.to_linear_order
(α : Type u_1)
[s : linear_ordered_comm_group_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 α] :
@[instance]
def
linear_ordered_comm_group_with_zero.to_ordered_comm_monoid
{α : Type u_1}
[linear_ordered_comm_group_with_zero α] :
Every linearly ordered commutative group with zero is an ordered commutative monoid.
Equations
- linear_ordered_comm_group_with_zero.to_ordered_comm_monoid = {mul := linear_ordered_comm_group_with_zero.mul _inst_1, mul_assoc := _, one := linear_ordered_comm_group_with_zero.one _inst_1, one_mul := _, mul_one := _, mul_comm := _, le := linear_ordered_comm_group_with_zero.le _inst_1, lt := linear_ordered_comm_group_with_zero.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, lt_of_mul_lt_mul_left := _}
theorem
one_le_pow_of_one_le'
{α : Type u_1}
[linear_ordered_comm_group_with_zero α]
{x : α}
{n : ℕ} :
theorem
pow_le_one_of_le_one
{α : Type u_1}
[linear_ordered_comm_group_with_zero α]
{x : α}
{n : ℕ} :
theorem
eq_one_of_pow_eq_one
{α : Type u_1}
[linear_ordered_comm_group_with_zero α]
{x : α}
{n : ℕ} :
@[simp]
@[simp]
@[simp]
@[simp]