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, LinearOrderedCommMonoidWithZero is defined in another file. However, the lemmas about it are stated here.

class LinearOrderedCommGroupWithZero (α : Type u_1) extends LinearOrderedCommMonoidWithZero , Inv , Div , Nontrivial : Type u_1

A linearly ordered commutative group with a zero element.

• 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 : α), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Monoid.npow (n + 1) x = x * Monoid.npow n x
• mul_comm : ∀ (a b : α), a * b = b * a
• 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
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a 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⁻¹

  a / b := a * b⁻¹

• zpow : ℤ → α → α

  The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α), LinearOrderedCommGroupWithZero.zpow 0 a = 1

  a ^ 0 = 1

• zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedCommGroupWithZero.zpow (Int.ofNat (Nat.succ n)) a = a * LinearOrderedCommGroupWithZero.zpow (Int.ofNat n) a

  a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedCommGroupWithZero.zpow (Int.negSucc n) a = (LinearOrderedCommGroupWithZero.zpow (↑(Nat.succ n)) a)⁻¹

  a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• inv_zero : 0⁻¹ = 0

  The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1

  Every nonzero element of a group with zero is invertible.

instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] : LinearOrderedCommMonoidWithZero (Multiplicative αᵒᵈ)

Equations

• One or more equations did not get rendered due to their size.

instance instLinearOrderedCommGroupWithZeroMultiplicativeOrderDual {α : Type u_1} [LinearOrderedAddCommGroupWithTop α] : LinearOrderedCommGroupWithZero (Multiplicative αᵒᵈ)

Equations

• One or more equations did not get rendered due to their size.

instance instLinearOrderedCommMonoidWithZeroWithZero {α : Type u_1} [LinearOrderedCommMonoid α] : LinearOrderedCommMonoidWithZero (WithZero α)

Equations

• One or more equations did not get rendered due to their size.

instance instLinearOrderedCommGroupWithZeroWithZero {α : Type u_1} [LinearOrderedCommGroup α] : LinearOrderedCommGroupWithZero (WithZero α)

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Function.Injective.linearOrderedCommMonoidWithZero {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {β : Type u_2} [Zero β] [One β] [Mul β] [Pow β ℕ] [Sup β] [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) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y)) : LinearOrderedCommMonoidWithZero β

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem zero_le' {α : Type u_1} {a : α} [LinearOrderedCommMonoidWithZero α] : 0 ≤ a

@[simp]

theorem not_lt_zero' {α : Type u_1} {a : α} [LinearOrderedCommMonoidWithZero α] : ¬a < 0

@[simp]

theorem le_zero_iff {α : Type u_1} {a : α} [LinearOrderedCommMonoidWithZero α] : a ≤ 0 ↔ a = 0

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

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

instance instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ)

Equations

• One or more equations did not get rendered due to their size.

theorem mul_le_one₀ {α : Type u_1} {a : α} {b : α} [LinearOrderedCommGroupWithZero α] (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1

Alias of mul_le_one' for unification.

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

Alias of one_le_mul' for unification.

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

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

theorem mul_inv_le_of_le_mul {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hab : a ≤ b * c) : a * c⁻¹ ≤ b

theorem inv_le_one₀ {α : Type u_1} {a : α} [LinearOrderedCommGroupWithZero α] (ha : a ≠ 0) : a⁻¹ ≤ 1 ↔ 1 ≤ a

theorem one_le_inv₀ {α : Type u_1} {a : α} [LinearOrderedCommGroupWithZero α] (ha : a ≠ 0) : 1 ≤ a⁻¹ ↔ a ≤ 1

theorem le_mul_inv_iff₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hc : c ≠ 0) : a ≤ b * c⁻¹ ↔ a * c ≤ b

theorem mul_inv_le_iff₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hc : c ≠ 0) : a * c⁻¹ ≤ b ↔ a ≤ b * c

theorem div_le_div₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] (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} [LinearOrderedCommGroupWithZero α] (u : αˣ) : 0 < ↑u

theorem mul_lt_mul_of_lt_of_le₀ {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [LinearOrderedCommGroupWithZero α] (hab : a ≤ b) (hb : b ≠ 0) (hcd : c < d) : a * c < b * d

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

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

theorem inv_mul_lt_of_lt_mul₀ {α : Type u_1} {x : α} {y : α} {z : α} [LinearOrderedCommGroupWithZero α] (h : x < y * z) : y⁻¹ * x < z

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

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

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

theorem lt_of_mul_lt_mul_of_le₀ {α : Type u_1} {a : α} {b : α} {c : α} {d : α} [LinearOrderedCommGroupWithZero α] (h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d

theorem mul_le_mul_right₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hc : c ≠ 0) : a * c ≤ b * c ↔ a ≤ b

theorem mul_le_mul_left₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (ha : a ≠ 0) : a * b ≤ a * c ↔ b ≤ c

theorem div_le_div_right₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hc : c ≠ 0) : a / c ≤ b / c ↔ a ≤ b

theorem div_le_div_left₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : a / b ≤ a / c ↔ c ≤ b

theorem le_div_iff₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hc : c ≠ 0) : a ≤ b / c ↔ a * c ≤ b

theorem div_le_iff₀ {α : Type u_1} {a : α} {b : α} {c : α} [LinearOrderedCommGroupWithZero α] (hc : c ≠ 0) : a / c ≤ b ↔ a ≤ b * c

@[simp]

theorem OrderIso.mulLeft₀'_toEquiv {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) : (OrderIso.mulLeft₀' ha).toEquiv = Equiv.mulLeft₀ a ha

@[simp]

theorem OrderIso.mulLeft₀'_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) (x : α) : (OrderIso.mulLeft₀' ha) x = a * x

def OrderIso.mulLeft₀' {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) : α ≃o α

Equiv.mulLeft₀ as an OrderIso on a LinearOrderedCommGroupWithZero..

Note that OrderIso.mulLeft₀ refers to the LinearOrderedField version.

Equations

• OrderIso.mulLeft₀' ha = let src := Equiv.mulLeft₀ a ha; { toEquiv := src, map_rel_iff' := (_ : ∀ {a_1 b : α}, ↑(Units.mk0 a ha) * a_1 ≤ ↑(Units.mk0 a ha) * b ↔ a_1 ≤ b) }

theorem OrderIso.mulLeft₀'_symm {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) : OrderIso.symm (OrderIso.mulLeft₀' ha) = OrderIso.mulLeft₀' (_ : a⁻¹ ≠ 0)

@[simp]

theorem OrderIso.mulRight₀'_toEquiv {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) : (OrderIso.mulRight₀' ha).toEquiv = Equiv.mulRight₀ a ha

@[simp]

theorem OrderIso.mulRight₀'_apply {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) (x : α) : (OrderIso.mulRight₀' ha) x = x * a

def OrderIso.mulRight₀' {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) : α ≃o α

Equiv.mulRight₀ as an OrderIso on a LinearOrderedCommGroupWithZero..

Note that OrderIso.mulRight₀ refers to the LinearOrderedField version.

Equations

• OrderIso.mulRight₀' ha = let src := Equiv.mulRight₀ a ha; { toEquiv := src, map_rel_iff' := (_ : ∀ {a_1 b : α}, a_1 * ↑(Units.mk0 a ha) ≤ b * ↑(Units.mk0 a ha) ↔ a_1 ≤ b) }

theorem OrderIso.mulRight₀'_symm {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} (ha : a ≠ 0) : OrderIso.symm (OrderIso.mulRight₀' ha) = OrderIso.mulRight₀' (_ : a⁻¹ ≠ 0)

instance instLinearOrderedAddCommGroupWithTopAdditiveOrderDual {α : Type u_1} [LinearOrderedCommGroupWithZero α] : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ)

Equations

• One or more equations did not get rendered due to their size.