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]
@[instance]
def
linear_ordered_comm_group_with_zero.to_comm_group_with_zero
(α : Type u_1)
[self : linear_ordered_comm_group_with_zero α] :
@[class]
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- 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
- max : α → α → α
- max_def : linear_ordered_comm_group_with_zero.max = max_default . "reflexivity"
- min : α → α → α
- min_def : linear_ordered_comm_group_with_zero.min = min_default . "reflexivity"
- 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 : α), 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 : α), c * a ≤ c * 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⁻¹) . "try_refl_tac"
- zpow : ℤ → α → α
- zpow_zero' : (∀ (a : α), linear_ordered_comm_group_with_zero.zpow 0 a = 1) . "try_refl_tac"
- zpow_succ' : (∀ (n : ℕ) (a : α), linear_ordered_comm_group_with_zero.zpow (int.of_nat n.succ) a = a * linear_ordered_comm_group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
- zpow_neg' : (∀ (n : ℕ) (a : α), linear_ordered_comm_group_with_zero.zpow -[1+ n] a = (linear_ordered_comm_group_with_zero.zpow ↑(n.succ) a)⁻¹) . "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.
@[protected, instance]
def
multiplicative.linear_ordered_comm_monoid_with_zero
{α : Type u_1}
[linear_ordered_add_comm_monoid_with_top α] :
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, max := max multiplicative.linear_order, max_def := _, min := min multiplicative.linear_order, min_def := _, 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 := _, zero := ⇑multiplicative.of_add ⊤, zero_mul := _, mul_zero := _, zero_le_one := _}
@[protected, instance]
def
multiplicative.linear_ordered_comm_group_with_zero
{α : Type u_1}
[linear_ordered_add_comm_group_with_top α] :
Equations
- multiplicative.linear_ordered_comm_group_with_zero = {le := linear_ordered_comm_monoid_with_zero.le multiplicative.linear_ordered_comm_monoid_with_zero, lt := linear_ordered_comm_monoid_with_zero.lt multiplicative.linear_ordered_comm_monoid_with_zero, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_comm_monoid_with_zero.decidable_le multiplicative.linear_ordered_comm_monoid_with_zero, decidable_eq := linear_ordered_comm_monoid_with_zero.decidable_eq multiplicative.linear_ordered_comm_monoid_with_zero, decidable_lt := linear_ordered_comm_monoid_with_zero.decidable_lt multiplicative.linear_ordered_comm_monoid_with_zero, max := linear_ordered_comm_monoid_with_zero.max multiplicative.linear_ordered_comm_monoid_with_zero, max_def := _, min := linear_ordered_comm_monoid_with_zero.min multiplicative.linear_ordered_comm_monoid_with_zero, min_def := _, mul := div_inv_monoid.mul multiplicative.div_inv_monoid, mul_assoc := _, one := div_inv_monoid.one multiplicative.div_inv_monoid, one_mul := _, mul_one := _, npow := div_inv_monoid.npow multiplicative.div_inv_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, zero := linear_ordered_comm_monoid_with_zero.zero multiplicative.linear_ordered_comm_monoid_with_zero, zero_mul := _, mul_zero := _, zero_le_one := _, inv := div_inv_monoid.inv multiplicative.div_inv_monoid, div := div_inv_monoid.div multiplicative.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow multiplicative.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, instance]
Equations
- with_zero.linear_ordered_comm_monoid_with_zero = {le := linear_order.le with_zero.linear_order, lt := linear_order.lt with_zero.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le with_zero.linear_order, decidable_eq := linear_order.decidable_eq with_zero.linear_order, decidable_lt := linear_order.decidable_lt with_zero.linear_order, max := max with_zero.linear_order, max_def := _, min := min with_zero.linear_order, min_def := _, mul := comm_monoid_with_zero.mul with_zero.comm_monoid_with_zero, mul_assoc := _, one := comm_monoid_with_zero.one with_zero.comm_monoid_with_zero, one_mul := _, mul_one := _, npow := comm_monoid_with_zero.npow with_zero.comm_monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, zero := comm_monoid_with_zero.zero with_zero.comm_monoid_with_zero, zero_mul := _, mul_zero := _, zero_le_one := _}
@[protected, instance]
Equations
- with_zero.linear_ordered_comm_group_with_zero = {le := linear_ordered_comm_monoid_with_zero.le with_zero.linear_ordered_comm_monoid_with_zero, lt := linear_ordered_comm_monoid_with_zero.lt with_zero.linear_ordered_comm_monoid_with_zero, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_comm_monoid_with_zero.decidable_le with_zero.linear_ordered_comm_monoid_with_zero, decidable_eq := linear_ordered_comm_monoid_with_zero.decidable_eq with_zero.linear_ordered_comm_monoid_with_zero, decidable_lt := linear_ordered_comm_monoid_with_zero.decidable_lt with_zero.linear_ordered_comm_monoid_with_zero, max := linear_ordered_comm_monoid_with_zero.max with_zero.linear_ordered_comm_monoid_with_zero, max_def := _, min := linear_ordered_comm_monoid_with_zero.min with_zero.linear_ordered_comm_monoid_with_zero, min_def := _, mul := linear_ordered_comm_monoid_with_zero.mul with_zero.linear_ordered_comm_monoid_with_zero, mul_assoc := _, one := linear_ordered_comm_monoid_with_zero.one with_zero.linear_ordered_comm_monoid_with_zero, one_mul := _, mul_one := _, npow := linear_ordered_comm_monoid_with_zero.npow with_zero.linear_ordered_comm_monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, zero := linear_ordered_comm_monoid_with_zero.zero with_zero.linear_ordered_comm_monoid_with_zero, zero_mul := _, mul_zero := _, zero_le_one := _, inv := comm_group_with_zero.inv with_zero.comm_group_with_zero, div := comm_group_with_zero.div with_zero.comm_group_with_zero, div_eq_mul_inv := _, zpow := comm_group_with_zero.zpow with_zero.comm_group_with_zero, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
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) :
Pullback a linear_ordered_comm_monoid_with_zero under an injective map.
See note [reducible non-instances].
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), max := max (linear_order.lift f hf), max_def := _, min := min (linear_order.lift f hf), min_def := _, 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 := _, zero := comm_monoid_with_zero.zero (function.injective.comm_monoid_with_zero f hf zero one mul), zero_mul := _, mul_zero := _, zero_le_one := _}
@[simp]
@[simp]
@[simp]
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) :
@[protected, instance]
def
additive.linear_ordered_add_comm_monoid_with_top
{α : Type u_1}
[linear_ordered_comm_monoid_with_zero α] :
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, max := max additive.linear_order, max_def := _, min := min additive.linear_order, min_def := _, 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 := _, top := 0, le_top := _, top_add' := _}
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) :
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) :
theorem
le_mul_inv_iff₀
{α : Type u_1}
{a b c : α}
[linear_ordered_comm_group_with_zero α]
(hc : c ≠ 0) :
theorem
mul_inv_le_iff₀
{α : Type u_1}
{a b c : α}
[linear_ordered_comm_group_with_zero α]
(hc : c ≠ 0) :
@[simp]
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) :
theorem
mul_lt_mul₀
{α : Type u_1}
{a b c d : α}
[linear_ordered_comm_group_with_zero α]
(hab : a < b)
(hcd : c < d) :
theorem
mul_inv_lt_of_lt_mul₀
{α : Type u_1}
{x y z : α}
[linear_ordered_comm_group_with_zero α]
(h : x < y * z) :
theorem
inv_mul_lt_of_lt_mul₀
{α : Type u_1}
{x y z : α}
[linear_ordered_comm_group_with_zero α]
(h : x < y * z) :
theorem
mul_lt_right₀
{α : Type u_1}
{a b : α}
[linear_ordered_comm_group_with_zero α]
(c : α)
(h : a < b)
(hc : c ≠ 0) :
theorem
pow_lt_pow_succ
{α : Type u_1}
[linear_ordered_comm_group_with_zero α]
{x : α}
{n : ℕ}
(hx : 1 < x) :
theorem
pow_lt_pow₀
{α : Type u_1}
[linear_ordered_comm_group_with_zero α]
{x : α}
{m n : ℕ}
(hx : 1 < x)
(hmn : m < n) :
theorem
inv_lt_inv₀
{α : Type u_1}
{a b : α}
[linear_ordered_comm_group_with_zero α]
(ha : a ≠ 0)
(hb : b ≠ 0) :
theorem
inv_le_inv₀
{α : Type u_1}
{a b : α}
[linear_ordered_comm_group_with_zero α]
(ha : a ≠ 0)
(hb : b ≠ 0) :
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
theorem
mul_le_mul_right₀
{α : Type u_1}
{a b c : α}
[linear_ordered_comm_group_with_zero α]
(hc : c ≠ 0) :
theorem
div_le_div_right₀
{α : Type u_1}
{a b c : α}
[linear_ordered_comm_group_with_zero α]
(hc : c ≠ 0) :
theorem
le_div_iff₀
{α : Type u_1}
{a b c : α}
[linear_ordered_comm_group_with_zero α]
(hc : c ≠ 0) :
theorem
div_le_iff₀
{α : Type u_1}
{a b c : α}
[linear_ordered_comm_group_with_zero α]
(hc : c ≠ 0) :
@[protected, instance]
def
additive.linear_ordered_add_comm_group_with_top
{α : Type u_1}
[linear_ordered_comm_group_with_zero α] :
Equations
- additive.linear_ordered_add_comm_group_with_top = {le := linear_ordered_add_comm_monoid_with_top.le additive.linear_ordered_add_comm_monoid_with_top, lt := linear_ordered_add_comm_monoid_with_top.lt additive.linear_ordered_add_comm_monoid_with_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_add_comm_monoid_with_top.decidable_le additive.linear_ordered_add_comm_monoid_with_top, decidable_eq := linear_ordered_add_comm_monoid_with_top.decidable_eq additive.linear_ordered_add_comm_monoid_with_top, decidable_lt := linear_ordered_add_comm_monoid_with_top.decidable_lt additive.linear_ordered_add_comm_monoid_with_top, max := linear_ordered_add_comm_monoid_with_top.max additive.linear_ordered_add_comm_monoid_with_top, max_def := _, min := linear_ordered_add_comm_monoid_with_top.min additive.linear_ordered_add_comm_monoid_with_top, min_def := _, add := sub_neg_monoid.add additive.sub_neg_monoid, add_assoc := _, zero := sub_neg_monoid.zero additive.sub_neg_monoid, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul additive.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, top := linear_ordered_add_comm_monoid_with_top.top additive.linear_ordered_add_comm_monoid_with_top, le_top := _, top_add' := _, neg := sub_neg_monoid.neg additive.sub_neg_monoid, sub := sub_neg_monoid.sub additive.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul additive.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, exists_pair_ne := _, neg_top := _, add_neg_cancel := _}
theorem
monoid_hom.map_neg_one
{α : Type u_1}
[linear_ordered_comm_group_with_zero α]
{R : Type u_2}
[ring R]
(f : R →* α) :
@[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) :
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) :