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_3) extends CommMonoidWithZero α, LinearOrder α, PosMulStrictMono α, OrderBot α : Type u_3

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
• zero : α
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• 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
• mul_lt_mul_of_pos_left ⦃a : α⦄ (ha : 0 < a) ⦃b c : α⦄ (hbc : b < c) : a * b < a * c
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• zero_le (a : α) : 0 ≤ a

class LinearOrderedCommGroupWithZero (α : Type u_3) extends LinearOrderedCommMonoidWithZero α, CommGroupWithZero α : Type u_3

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
• zero : α
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• 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
• mul_lt_mul_of_pos_left ⦃a : α⦄ (ha : 0 < a) ⦃b c : α⦄ (hbc : b < c) : a * b < a * c
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• zero_le (a : α) : 0 ≤ a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : LinearOrderedCommGroupWithZero.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : LinearOrderedCommGroupWithZero.zpow (↑n.succ) a = LinearOrderedCommGroupWithZero.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : LinearOrderedCommGroupWithZero.zpow (Int.negSucc n) a = (LinearOrderedCommGroupWithZero.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel (a : α) : a ≠ 0 → a * a⁻¹ = 1

The following facts are true more generally in a (linearly) ordered commutative monoid.

@[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

theorem bot_eq_zero'' {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : ⊥ = 0

See also bot_eq_zero and bot_eq_zero' for canonically ordered monoids.

@[instance 100]

instance LinearOrderedCommMonoidWithZero.toZeroLeOneClass {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : ZeroLEOneClass α

@[instance 100]

instance LinearOrderedCommMonoidWithZero.toMulPosStrictMono {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : MulPosStrictMono α

@[instance 100]

instance LinearOrderedCommMonoidWithZero.toIsOrderedMonoid {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : IsOrderedMonoid α

@[instance 100]

instance instIsCancelMulZero_1 {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : IsCancelMulZero α

@[reducible, inline]

abbrev Function.Injective.linearOrderedCommMonoidWithZero {α : Type u_1} [LinearOrderedCommMonoidWithZero α] {β : Type u_3} [Zero β] [Bot β] [One β] [Mul β] [Pow β ℕ] [LE β] [LT β] [Max β] [Min β] [Ord β] [DecidableEq β] [DecidableLE β] [DecidableLT β] (f : β → α) (hf : 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) (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : β}, f x < f y ↔ x < y) (hsup : ∀ (x y : β), f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y)) (bot : f ⊥ = ⊥) (compare : ∀ (x y : β), compare (f x) (f y) = compare x y) : LinearOrderedCommMonoidWithZero β

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

@[instance 100]

instance LinearOrderedCommMonoidWithZero.toIsMulTorsionFree {α : Type u_1} [LinearOrderedCommMonoidWithZero α] : IsMulTorsionFree α

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

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

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

@[simp]

theorem Units.zero_lt {α : Type u_1} [LinearOrderedCommGroupWithZero α] (u : αˣ) : 0 < ↑u

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 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

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

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

theorem denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units {α : Type u_1} [LinearOrderedCommGroupWithZero α] : DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ

instance instNontrivialUnitsOfDenselyOrdered {α : Type u_1} [LinearOrderedCommGroupWithZero α] [DenselyOrdered α] : Nontrivial αˣ

instance instDenselyOrderedUnits {α : Type u_1} [LinearOrderedCommGroupWithZero α] [DenselyOrdered α] : DenselyOrdered αˣ

theorem denselyOrdered_units_iff {α : Type u_1} [LinearOrderedCommGroupWithZero α] [Nontrivial αˣ] : DenselyOrdered αˣ ↔ DenselyOrdered α

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

@[deprecated "Use simp" (since := "2025-11-17")]

theorem ofAdd_toDual_eq_zero_iff {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (x : α) : Multiplicative.ofAdd (OrderDual.toDual x) = 0 ↔ x = ⊤

@[deprecated "Use simp" (since := "2025-11-17")]

theorem ofDual_toAdd_eq_top_iff {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] (x : Multiplicative αᵒᵈ) : OrderDual.ofDual (Multiplicative.toAdd x) = ⊤ ↔ x = 0

@[deprecated bot_eq_zero'' (since := "2025-11-17")]

theorem ofAdd_bot {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] : Multiplicative.ofAdd ⊥ = 0

@[simp]

theorem ofDual_toAdd_zero {α : Type u_1} [LinearOrderedAddCommMonoidWithTop α] : OrderDual.ofDual (Multiplicative.toAdd 0) = ⊤

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

instance WithZero.instBot {α : Type u_1} : Bot (WithZero α)

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

@[instance 10]

instance WithZero.le {α : Type u_1} [LE α] : LE (WithZero α)

theorem WithZero.le_def {α : Type u_1} [LE α] {x y : WithZero α} : x ≤ y ↔ ∀ (a : α), x = ↑a → ∃ (b : α), y = ↑b ∧ a ≤ b

@[simp]

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

theorem WithZero.not_coe_le_zero {α : Type u_1} [LE α] (a : α) : ¬↑a ≤ 0

instance WithZero.instOrderBot {α : Type u_1} [LE α] : OrderBot (WithZero α)

instance WithZero.instBoundedOrder {α : Type u_1} [LE α] [OrderTop α] : BoundedOrder (WithBot α)

@[simp]

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

@[simp]

theorem WithZero.nonpos_iff_eq_zero {α : Type u_1} [LE α] {x : WithZero α} : x ≤ 0 ↔ x = 0

There is a general version le_zero_iff, but this lemma does not require a PartialOrder.

theorem WithZero.coe_le_iff {α : Type u_1} [LE α] {x : WithZero α} {a : α} : ↑a ≤ x ↔ ∃ (b : α), x = ↑b ∧ a ≤ b

theorem WithZero.le_coe_iff {α : Type u_1} [LE α] {x : WithZero α} {b : α} : x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b

theorem IsMax.withZero {α : Type u_1} [LE α] {a : α} (h : IsMax a) : IsMax ↑a

theorem WithZero.le_unzero_iff {α : Type u_1} [LE α] {y : WithZero α} {a : α} (hy : y ≠ 0) : a ≤ unzero hy ↔ ↑a ≤ y

theorem WithZero.unbot_le_iff {α : Type u_1} [LE α] {x : WithZero α} {b : α} (hx : x ≠ 0) : unzero hx ≤ b ↔ x ≤ ↑b

@[simp]

theorem WithZero.one_le_coe {α : Type u_1} [LE α] {a : α} [One α] : 1 ≤ ↑a ↔ 1 ≤ a

@[simp]

theorem WithZero.coe_le_one {α : Type u_1} [LE α] {a : α} [One α] : ↑a ≤ 1 ↔ a ≤ 1

@[simp]

theorem WithZero.unzero_le_unzero {α : Type u_1} [LE α] {x y : WithZero α} (hx : x ≠ 0) (hy : y ≠ 0) : unzero hx ≤ unzero hy ↔ x ≤ y

@[instance 10]

instance WithZero.instLT {α : Type u_1} [LT α] : LT (WithZero α)

The order on WithZero α, defined by ⊥ < ↑a and a < b → ↑a < ↑b.

theorem WithZero.lt_def {α : Type u_1} [LT α] {x y : WithZero α} : x < y ↔ (x = 0 ∧ ∃ (b : α), y = ↑b) ∨ ∃ (a : α) (b : α), a < b ∧ x = ↑a ∧ y = ↑b

theorem WithZero.lt_iff_exists {α : Type u_1} [LT α] {x y : WithZero α} : x < y ↔ ∃ (b : α), y = ↑b ∧ ∀ (a : α), x = ↑a → a < b

@[simp]

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

@[simp]

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

@[simp]

theorem WithZero.not_lt_zero {α : Type u_1} [LT α] (a : WithZero α) : ¬a < 0

theorem WithZero.lt_iff_exists_coe {α : Type u_1} [LT α] {x y : WithZero α} : x < y ↔ ∃ (b : α), y = ↑b ∧ x < ↑b

theorem WithZero.lt_coe_iff {α : Type u_1} [LT α] {x : WithZero α} {b : α} : x < ↑b ↔ ∀ (a : α), x = ↑a → a < b

theorem WithZero.pos_iff_ne_zero {α : Type u_1} [LT α] {x : WithZero α} : 0 < x ↔ x ≠ 0

A version of pos_iff_ne_zero for WithZero that only requires LT α, not PartialOrder α.

theorem WithZero.lt_unzero_iff {α : Type u_1} [LT α] {y : WithZero α} {a : α} (hy : y ≠ 0) : a < unzero hy ↔ ↑a < y

theorem WithZero.unzero_lt_iff {α : Type u_1} [LT α] {x : WithZero α} {b : α} (hx : x ≠ 0) : unzero hx < b ↔ x < ↑b

@[simp]

theorem WithZero.one_lt_coe {α : Type u_1} [LT α] {a : α} [One α] : 1 < ↑a ↔ 1 < a

@[simp]

theorem WithZero.coe_lt_one {α : Type u_1} [LT α] {a : α} [One α] : ↑a < 1 ↔ a < 1

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

instance WithZero.instMulLeftMono {α : Type u_1} [Preorder α] [Mul α] [MulLeftMono α] : MulLeftMono (WithZero α)

theorem WithZero.addLeftMono {α : Type u_1} [Preorder α] [AddZeroClass α] [AddLeftMono α] (h : ∀ (a : α), 0 ≤ a) : AddLeftMono (WithZero α)

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

theorem WithZero.map'_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : Monotone ⇑f) : Monotone ⇑(map' f)

theorem WithZero.map'_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : StrictMono ⇑f) : StrictMono ⇑(map' f)

theorem WithZero.exists_ne_zero_and_lt {α : Type u_1} [Preorder α] {x : WithZero α} [NoMinOrder α] (hx : x ≠ 0) : ∃ (y : WithZero α), y ≠ 0 ∧ y < x

theorem WithZero.toAdd_unzero_lt_of_lt_ofAdd {α : Type u_1} [Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) (h : a < ↑(Multiplicative.ofAdd b)) : Multiplicative.toAdd (unzero ha) < b

theorem WithZero.lt_ofAdd_of_toAdd_unzero_lt {α : Type u_1} [Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) (h : Multiplicative.toAdd (unzero ha) < b) : a < ↑(Multiplicative.ofAdd b)

theorem WithZero.lt_ofAdd_iff {α : Type u_1} [Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) : a < ↑(Multiplicative.ofAdd b) ↔ Multiplicative.toAdd (unzero ha) < b

theorem WithZero.toAdd_unzero_le_of_lt_ofAdd {α : Type u_1} [Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) (h : a ≤ ↑(Multiplicative.ofAdd b)) : Multiplicative.toAdd (unzero ha) ≤ b

theorem WithZero.le_ofAdd_of_toAdd_unzero_le {α : Type u_1} [Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) (h : Multiplicative.toAdd (unzero ha) ≤ b) : a ≤ ↑(Multiplicative.ofAdd b)

theorem WithZero.le_ofAdd_iff {α : Type u_1} [Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) : a ≤ ↑(Multiplicative.ofAdd b) ↔ Multiplicative.toAdd (unzero ha) ≤ b

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

instance WithZero.instMulLeftReflectLT {α : Type u_1} [PartialOrder α] [Mul α] [MulLeftReflectLT α] : MulLeftReflectLT (WithZero α)

instance WithZero.semilatticeSup {α : Type u_1} [SemilatticeSup α] : SemilatticeSup (WithZero α)

theorem WithZero.coe_sup {α : Type u_1} [SemilatticeSup α] (a b : α) : ↑(a ⊔ b) = ↑a ⊔ ↑b

instance WithZero.semilatticeInf {α : Type u_1} [SemilatticeInf α] : SemilatticeInf (WithZero α)

theorem WithZero.coe_inf {α : Type u_1} [SemilatticeInf α] (a b : α) : ↑(a ⊓ b) = ↑a ⊓ ↑b

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

instance WithZero.decidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (WithZero α)

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

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

instance WithZero.total_le {α : Type u_1} [Preorder α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : Std.Total fun (x1 x2 : WithZero α) => x1 ≤ x2

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

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

theorem WithZero.exists_ne_zero_and_le_and_le {α : Type u_1} [LinearOrder α] {x y : WithZero α} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (z : WithZero α), z ≠ 0 ∧ z ≤ x ∧ z ≤ y

theorem WithZero.exists_ne_zero_and_lt_and_lt {α : Type u_1} [LinearOrder α] {x y : WithZero α} [NoMinOrder α] (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (z : WithZero α), z ≠ 0 ∧ z < x ∧ z < y

instance WithZero.isOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid (WithZero α)

theorem WithZero.isOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (zero_le : ∀ (a : α), 0 ≤ a) : IsOrderedAddMonoid (WithZero α)

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

instance WithZero.instCanonicallyOrderedAdd {α : Type u_1} [AddZeroClass α] [Preorder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedAdd (WithZero α)

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

instance WithZero.instLinearOrderedCommMonoidWithZero {α : Type u_1} [CommMonoid α] [LinearOrder α] [IsOrderedCancelMonoid α] : LinearOrderedCommMonoidWithZero (WithZero α)

instance WithZero.instLinearOrderedCommGroupWithZero {α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] : LinearOrderedCommGroupWithZero (WithZero α)

Exponential and logarithm

@[simp]

theorem WithZero.exp_le_exp {G : Type u_3} [Preorder G] {a b : G} : exp a ≤ exp b ↔ a ≤ b

@[simp]

theorem WithZero.exp_lt_exp {G : Type u_3} [Preorder G] {a b : G} : exp a < exp b ↔ a < b

@[simp]

theorem WithZero.exp_pos {G : Type u_3} [Preorder G] {a : G} : 0 < exp a

@[simp]

theorem WithZero.log_le_log {G : Type u_3} [Preorder G] [AddGroup G] {x y : WithZero (Multiplicative G)} (hx : x ≠ 0) (hy : y ≠ 0) : x.log ≤ y.log ↔ x ≤ y

@[simp]

theorem WithZero.log_lt_log {G : Type u_3} [Preorder G] [AddGroup G] {x y : WithZero (Multiplicative G)} (hx : x ≠ 0) (hy : y ≠ 0) : x.log < y.log ↔ x < y

theorem WithZero.log_le_iff_le_exp {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x ≠ 0) : x.log ≤ a ↔ x ≤ exp a

theorem WithZero.log_lt_iff_lt_exp {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x ≠ 0) : x.log < a ↔ x < exp a

theorem WithZero.le_log_iff_exp_le {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x ≠ 0) : a ≤ x.log ↔ exp a ≤ x

theorem WithZero.lt_log_iff_exp_lt {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hx : x ≠ 0) : a < x.log ↔ exp a < x

theorem WithZero.le_exp_of_log_le {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hxa : x.log ≤ a) : x ≤ exp a

theorem WithZero.lt_exp_of_log_lt {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hxa : x.log < a) : x < exp a

theorem WithZero.le_log_of_exp_le {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hax : exp a ≤ x) : a ≤ x.log

theorem WithZero.lt_log_of_exp_lt {G : Type u_3} [Preorder G] {a : G} [AddGroup G] {x : WithZero (Multiplicative G)} (hax : exp a < x) : a < x.log

def WithZero.expOrderIso {G : Type u_3} [Preorder G] [AddGroup G] : G ≃o (WithZero (Multiplicative G))ˣ

The exponential map as an order isomorphism between G and Gᵐ⁰ˣ.

@[simp]

theorem WithZero.val_inv_expOrderIso_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) : ↑(expOrderIso a✝)⁻¹ = (↑(Multiplicative.ofAdd a✝))⁻¹

@[simp]

theorem WithZero.val_expOrderIso_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) : ↑(expOrderIso a✝) = ↑(Multiplicative.ofAdd a✝)

@[simp]

theorem WithZero.expOrderIso_symm_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : (WithZero (Multiplicative G))ˣ) : (RelIso.symm expOrderIso) a✝ = Multiplicative.toAdd (unzero ⋯)

def WithZero.logOrderIso {G : Type u_3} [Preorder G] [AddGroup G] : (WithZero (Multiplicative G))ˣ ≃o G

The logarithm as an order isomorphism between Gᵐ⁰ˣ and G.

@[simp]

theorem WithZero.logOrderIso_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : (WithZero (Multiplicative G))ˣ) : logOrderIso a✝ = Multiplicative.toAdd (unzero ⋯)

@[simp]

theorem WithZero.val_logOrderIso_symm_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) : ↑((RelIso.symm logOrderIso) a✝) = ↑(Multiplicative.ofAdd a✝)

@[simp]

theorem WithZero.val_inv_logOrderIso_symm_apply {G : Type u_3} [Preorder G] [AddGroup G] (a✝ : G) : ↑((RelIso.symm logOrderIso) a✝)⁻¹ = (↑(Multiplicative.ofAdd a✝))⁻¹

theorem WithZero.lt_mul_exp_iff_le {x y : WithZero (Multiplicative ℤ)} (hy : y ≠ 0) : x < y * exp 1 ↔ x ≤ y

theorem WithZero.le_exp_log {G : Type u_3} [Preorder G] [AddGroup G] {x : WithZero (Multiplicative G)} : x ≤ exp x.log