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.

class LinearOrderedCommMonoidWithZero (α : Type u_2) extends LinearOrderedCommMonoid , Zero : Type u_2

A linearly ordered commutative monoid 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 = Monoid.npow n x * 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

  Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : α), a * 0 = 0

  Zero is a right absorbing element for multiplication

• zero_le_one : 0 ≤ 1

  0 ≤ 1 in any linearly ordered commutative monoid.

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

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 = Monoid.npow n x * 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 = LinearOrderedCommGroupWithZero.zpow (Int.ofNat n) a * a

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

• 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 LinearOrderedCommMonoidWithZero.toZeroLeOneClass {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : ZeroLEOneClass α

Equations

• ⋯ = ⋯

instance canonicallyOrderedAddCommMonoid.toZeroLeOneClass {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] [One α] : ZeroLEOneClass α

Equations

• ⋯ = ⋯

@[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} [LinearOrderedCommMonoidWithZero α] {a : α} : 0 ≤ a

@[simp]

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

@[simp]

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

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

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

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

Equations

• instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual = let __src := Additive.orderedAddCommMonoid; let __src_1 := Additive.linearOrder; LinearOrderedAddCommMonoidWithTop.mk ⋯

theorem pow_pos_iff {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {a : α} {n : ℕ} [NoZeroDivisors α] (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a

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

Alias of mul_le_one' for unification.

theorem one_le_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} (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} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (h : c ≠ 0) (hab : a * c ≤ b * c) : a ≤ b

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

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

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

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

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

theorem mul_inv_le_iff₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (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} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} {d : α} (hab : a ≤ b) (hb : b ≠ 0) (hcd : c < d) : a * c < b * d

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

theorem mul_inv_lt_of_lt_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (h : a < b * c) : a * c⁻¹ < b

theorem inv_mul_lt_of_lt_mul₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {b : α} {c : α} (h : a < b * c) : b⁻¹ * a < c

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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' := ⋯ }

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

@[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' := ⋯ }

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

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

Equations

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

theorem pow_lt_pow_succ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {n : ℕ} (ha : 1 < a) : a ^ n < a ^ Nat.succ n

theorem pow_lt_pow_right₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {m : ℕ} {n : ℕ} (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n

@[deprecated pow_lt_pow_right₀]

theorem pow_lt_pow₀ {α : Type u_1} [LinearOrderedCommGroupWithZero α] {a : α} {m : ℕ} {n : ℕ} (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n

Alias of pow_lt_pow_right₀.

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

Equations

• instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual = let __src := Multiplicative.orderedCommMonoid; let __src_1 := Multiplicative.linearOrder; LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯

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

Equations

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

instance WithZero.preorder {α : Type u_1} [Preorder α] : Preorder (WithZero α)

Equations

• WithZero.preorder = WithBot.preorder

instance WithZero.orderBot {α : Type u_1} [Preorder α] : OrderBot (WithZero α)

Equations

• WithZero.orderBot = WithBot.orderBot

theorem WithZero.zero_le {α : Type u_1} [Preorder α] (a : WithZero α) : 0 ≤ a

theorem WithZero.zero_lt_coe {α : Type u_1} [Preorder α] (a : α) : 0 < ↑a

theorem WithZero.zero_eq_bot {α : Type u_1} [Preorder α] : 0 = ⊥

@[simp]

theorem WithZero.coe_lt_coe {α : Type u_1} [Preorder α] {a : α} {b : α} : ↑a < ↑b ↔ a < b

@[simp]

theorem WithZero.coe_le_coe {α : Type u_1} [Preorder α] {a : α} {b : α} : ↑a ≤ ↑b ↔ a ≤ b

instance WithZero.covariantClass_mul_le {α : Type u_1} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : CovariantClass (WithZero α) (WithZero α) (fun (x x_1 : WithZero α) => x * x_1) fun (x x_1 : WithZero α) => x ≤ x_1

Equations

• ⋯ = ⋯

theorem WithZero.covariantClass_add_le {α : Type u_1} [Preorder α] [AddZeroClass α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : ∀ (a : α), 0 ≤ a) : CovariantClass (WithZero α) (WithZero α) (fun (x x_1 : WithZero α) => x + x_1) fun (x x_1 : WithZero α) => x ≤ x_1

instance WithZero.existsAddOfLE {α : Type u_1} [Preorder α] [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithZero α)

Equations

• ⋯ = ⋯

instance WithZero.partialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (WithZero α)

Equations

• WithZero.partialOrder = WithBot.partialOrder

instance WithZero.contravariantClass_mul_lt {α : Type u_1} [PartialOrder α] [Mul α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] : ContravariantClass (WithZero α) (WithZero α) (fun (x x_1 : WithZero α) => x * x_1) fun (x x_1 : WithZero α) => x < x_1

Equations

• ⋯ = ⋯

instance WithZero.lattice {α : Type u_1} [Lattice α] : Lattice (WithZero α)

Equations

• WithZero.lattice = WithBot.lattice

instance WithZero.linearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (WithZero α)

Equations

• WithZero.linearOrder = WithBot.linearOrder

theorem WithZero.le_max_iff {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} : ↑a ≤ max ↑b ↑c ↔ a ≤ max b c

theorem WithZero.min_le_iff {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} : min ↑a ↑b ≤ ↑c ↔ min a b ≤ c

instance WithZero.orderedCommMonoid {α : Type u_1} [OrderedCommMonoid α] : OrderedCommMonoid (WithZero α)

Equations

• WithZero.orderedCommMonoid = let __src := CommMonoidWithZero.toCommMonoid; let __src_1 := WithZero.partialOrder; OrderedCommMonoid.mk ⋯

@[reducible]

def WithZero.orderedAddCommMonoid {α : Type u_1} [OrderedAddCommMonoid α] (zero_le : ∀ (a : α), 0 ≤ a) : OrderedAddCommMonoid (WithZero α)

If 0 is the least element in α, then WithZero α is an OrderedAddCommMonoid.

Equations

• WithZero.orderedAddCommMonoid zero_le = let __src := WithZero.partialOrder; let __src_1 := WithZero.addCommMonoid; OrderedAddCommMonoid.mk ⋯

instance WithZero.canonicallyOrderedAddCommMonoid {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] : CanonicallyOrderedAddCommMonoid (WithZero α)

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations

• WithZero.canonicallyOrderedAddCommMonoid = let __src := WithZero.orderBot; let __src_1 := WithZero.orderedAddCommMonoid ⋯; let __src_2 := ⋯; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯

instance WithZero.canonicallyLinearOrderedAddCommMonoid {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] : CanonicallyLinearOrderedAddCommMonoid (WithZero α)

Equations

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

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

Equations

• WithZero.instLinearOrderedCommMonoidWithZero = let __src := WithZero.linearOrder; let __src_1 := WithZero.commMonoidWithZero; LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯

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

Equations

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