doc-next-gen

Mathlib.Algebra.Order.GroupWithZero.Canonical

Module docstring

{"# 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. "}

LinearOrderedCommMonoidWithZero structure
(α : Type*) extends CommMonoidWithZero α, LinearOrder α, IsOrderedMonoid α, OrderBot α
Full source 
/-- A linearly ordered commutative monoid with a zero element. -/
class LinearOrderedCommMonoidWithZero (α : Type*) extends CommMonoidWithZero α, LinearOrder α,
    IsOrderedMonoid α, OrderBot α where
  /-- `0 ≤ 1` in any linearly ordered commutative monoid. -/
  zero_le_one : (0 : α) ≤ 1
Linearly Ordered Commutative Monoid with Zero
Informal description
A structure representing a linearly ordered commutative monoid with a zero element adjoined. This structure combines the properties of a commutative monoid with zero, a linear order, and the condition that the order is compatible with the monoid operation (i.e., multiplication by a non-negative element preserves the order). Additionally, it includes the property that zero is the least element in the order.
LinearOrderedCommGroupWithZero structure
(α : Type*) extends LinearOrderedCommMonoidWithZero α, CommGroupWithZero α
Full source 
/-- A linearly ordered commutative group with a zero element. -/
class LinearOrderedCommGroupWithZero (α : Type*) extends LinearOrderedCommMonoidWithZero α,
  CommGroupWithZero α
Linearly Ordered Commutative Group with Zero
Informal description
A linearly ordered commutative group with a zero element adjoined. This structure combines the properties of a linearly ordered commutative monoid with zero and a commutative group with zero, providing a unified framework for algebraic structures that commonly appear as valuation targets in number theory.
LinearOrderedCommMonoidWithZero.toZeroLeOneClass instance
[LinearOrderedCommMonoidWithZero α] : ZeroLEOneClass α
Full source 
instance (priority := 100) LinearOrderedCommMonoidWithZero.toZeroLeOneClass
    [LinearOrderedCommMonoidWithZero α] : ZeroLEOneClass α :=
  { ‹LinearOrderedCommMonoidWithZero α› with }
Zero is Less Than or Equal to One in Linearly Ordered Commutative Monoids with Zero
Informal description
Every linearly ordered commutative monoid with zero satisfies $0 \leq 1$.
CanonicallyOrderedAdd.toZeroLeOneClass instance
[AddZeroClass α] [LE α] [CanonicallyOrderedAdd α] [One α] : ZeroLEOneClass α
Full source 
instance (priority := 100) CanonicallyOrderedAdd.toZeroLeOneClass
    [AddZeroClass α] [LE α] [CanonicallyOrderedAdd α] [One α] : ZeroLEOneClass α :=
  ⟨zero_le 1⟩
Zero is Less Than or Equal to One in Canonically Ordered Additive Monoids
Informal description
For any additively canonically ordered monoid $\alpha$ with a zero element and a one element, the inequality $0 \leq 1$ holds.
Function.Injective.linearOrderedCommMonoidWithZero abbrev
{β : Type*} [Zero β] [Bot β] [One β] [Mul β] [Pow β ℕ] [Max β] [Min β] (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)) (bot : f ⊥ = ⊥) : LinearOrderedCommMonoidWithZero β
Full source 
/-- Pullback a `LinearOrderedCommMonoidWithZero` under an injective map.
See note [reducible non-instances]. -/
abbrev Function.Injective.linearOrderedCommMonoidWithZero {β : Type*} [Zero β] [Bot β] [One β]
    [Mul β] [Pow β ℕ] [Max β] [Min β] (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))
    (bot : f ⊥ = ⊥) : LinearOrderedCommMonoidWithZero β where
  __ := LinearOrder.lift f hf hsup hinf
  __ := hf.isOrderedMonoid f one mul npow
  __ := hf.commMonoidWithZero f zero one mul npow
  zero_le_one :=
      show f 0 ≤ f 1 by simp only [zero, one, LinearOrderedCommMonoidWithZero.zero_le_one]
  bot_le a := show f ⊥ ≤ f a from bot ▸ bot_le
Pullback of Linearly Ordered Commutative Monoid with Zero Structure via Injective Function
Informal description
Let $\beta$ be a type equipped with operations for zero, bottom, one, multiplication, exponentiation by natural numbers, maximum, and minimum. Given an injective function $f \colon \beta \to \alpha$ from $\beta$ to a linearly ordered commutative monoid with zero $\alpha$, such that: - $f$ preserves zero: $f(0) = 0$, - $f$ preserves one: $f(1) = 1$, - $f$ preserves multiplication: $f(x * y) = f(x) * f(y)$ for all $x, y \in \beta$, - $f$ preserves exponentiation: $f(x^n) = f(x)^n$ for all $x \in \beta$ and $n \in \mathbb{N}$, - $f$ preserves suprema: $f(x \sqcup y) = \max(f(x), f(y))$ for all $x, y \in \beta$, - $f$ preserves infima: $f(x \sqcap y) = \min(f(x), f(y))$ for all $x, y \in \beta$, - $f$ preserves the bottom element: $f(\bot) = \bot$, then $\beta$ inherits the structure of a linearly ordered commutative monoid with zero from $\alpha$ via $f$.
zero_le' theorem
: 0 ≤ a
Full source 
@[simp] lemma zero_le' : 0 ≤ a := by
  simpa only [mul_zero, mul_one] using mul_le_mul_left' (zero_le_one' α) a
Nonnegativity of Elements in Linearly Ordered Commutative Monoids with Zero
Informal description
For any element $a$ in a linearly ordered commutative monoid with zero, the zero element is less than or equal to $a$, i.e., $0 \leq a$.
not_lt_zero' theorem
: ¬a < 0
Full source 
@[simp]
theorem not_lt_zero' : ¬a < 0 :=
  not_lt_of_le zero_le'
Nonnegativity in Linearly Ordered Commutative Monoids with Zero: $\neg (a < 0)$
Informal description
For any element $a$ in a linearly ordered commutative monoid with zero, it is not the case that $a$ is strictly less than zero.
zero_lt_iff theorem
: 0 < a ↔ a ≠ 0
Full source 
theorem zero_lt_iff : 0 < a ↔ a ≠ 0 :=
  ⟨ne_of_gt, fun h ↦ lt_of_le_of_ne zero_le' h.symm⟩
Strict Positivity Criterion in Linearly Ordered Commutative Monoids with Zero
Informal description
For any element $a$ in a linearly ordered commutative monoid with zero, the zero element is strictly less than $a$ if and only if $a$ is not equal to zero, i.e., $0 < a \leftrightarrow a \neq 0$.
ne_zero_of_lt theorem
(h : b < a) : a ≠ 0
Full source 
theorem ne_zero_of_lt (h : b < a) : a ≠ 0 := fun h1 ↦ not_lt_zero' <| show b < 0 from h1 ▸ h
Nonzero Element from Strict Inequality: $b < a \Rightarrow a \neq 0$
Informal description
For any elements $a$ and $b$ in a linearly ordered commutative monoid with zero, if $b < a$, then $a$ is not equal to zero.
bot_eq_zero'' theorem
: (⊥ : α) = 0
Full source 
/-- See also `bot_eq_zero` and `bot_eq_zero'` for canonically ordered monoids. -/
lemma bot_eq_zero'' : (⊥ : α) = 0 := eq_of_forall_ge_iff fun _ ↦ by simp
Bottom Element Equals Zero in Linearly Ordered Commutative Monoid with Zero
Informal description
In a linearly ordered commutative monoid with zero $\alpha$, the bottom element $\bot$ is equal to the zero element $0$.
instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual instance
: LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ)
Full source 
instance instLinearOrderedAddCommMonoidWithTopAdditiveOrderDual :
    LinearOrderedAddCommMonoidWithTop (Additive αᵒᵈ) where
  top := .ofMul <| .toDual 0
  top_add' a := zero_mul a.toMul.ofDual
  le_top _ := zero_le'
Additive Order Dual of a Linearly Ordered Commutative Monoid with Zero is a Linearly Ordered Commutative Additive Monoid with Top
Informal description
For any linearly ordered commutative monoid with zero $\alpha$, the additive monoid of its order dual $\alpha^{\text{op}}$ is a linearly ordered commutative additive monoid with top.
instLinearOrderedAddCommMonoidWithTopOrderDualAdditive instance
: LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ
Full source 
instance instLinearOrderedAddCommMonoidWithTopOrderDualAdditive :
    LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ where
  top := .toDual <| .ofMul _
  top_add' := fun a ↦ zero_mul (Additive.toMul (OrderDual.ofDual a))
  le_top := fun a ↦ @zero_le' _ _ (Additive.toMul (OrderDual.ofDual a))
Order Dual of Additive Monoid as Linearly Ordered Commutative Additive Monoid with Top
Informal description
The order dual of the additive monoid of a linearly ordered commutative monoid with zero is a linearly ordered commutative additive monoid with top.
pow_pos_iff theorem
(hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a
Full source 
lemma pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn]
Positivity of Powers in Linearly Ordered Commutative Monoids with Zero: $0 < a^n \leftrightarrow 0 < a$ for $n \neq 0$
Informal description
For any element $a$ in a linearly ordered commutative monoid with zero and any nonzero exponent $n$, the power $a^n$ is positive if and only if $a$ is positive. That is, $0 < a^n \leftrightarrow 0 < a$.
LinearOrderedCommGroupWithZero.toMulPosMono instance
: MulPosMono α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toMulPosMono : MulPosMono α where
  elim _a _b _c hbc := mul_le_mul_right' hbc _
Monotonicity of Right Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
Every linearly ordered commutative group with zero $\alpha$ satisfies the property that right multiplication by nonnegative elements is monotone. That is, for any nonnegative element $b \in \alpha$, if $a_1 \leq a_2$, then $a_1 * b \leq a_2 * b$.
LinearOrderedCommGroupWithZero.toPosMulMono instance
: PosMulMono α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toPosMulMono : PosMulMono α where
  elim _a _b _c hbc := mul_le_mul_left' hbc _
Monotonicity of Left Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
For any linearly ordered commutative group with zero $\alpha$, left multiplication by nonnegative elements is monotone. That is, for any $b \geq 0$ and any $a_1 \leq a_2$ in $\alpha$, we have $b \cdot a_1 \leq b \cdot a_2$.
LinearOrderedCommGroupWithZero.toPosMulReflectLE instance
: PosMulReflectLE α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toPosMulReflectLE :
    PosMulReflectLE α where
  elim a b c hbc := by simpa [a.2.ne'] using mul_le_mul_left' hbc a⁻¹
Reflection of Order by Positive Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
For any linearly ordered commutative group with zero $\alpha$, multiplication by a positive element reflects the order relation $\leq$. That is, for any positive element $b \in \alpha$ and any elements $a_1, a_2 \in \alpha$, if $b \cdot a_1 \leq b \cdot a_2$, then $a_1 \leq a_2$.
LinearOrderedCommGroupWithZero.toMulPosReflectLE instance
: MulPosReflectLE α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toMulPosReflectLE :
    MulPosReflectLE α where
  elim a b c hbc := by simpa [a.2.ne'] using mul_le_mul_right' hbc a⁻¹
Reflection of Order under Right Multiplication by Positive Elements in Linearly Ordered Commutative Groups with Zero
Informal description
For any linearly ordered commutative group with zero $\alpha$, right multiplication by a positive element reflects the non-strict order relation. That is, for any $b > 0$ in $\alpha$, if $a_1 \cdot b \leq a_2 \cdot b$, then $a_1 \leq a_2$.
LinearOrderedCommGroupWithZero.toPosMulReflectLT instance
: PosMulReflectLT α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toPosMulReflectLT :
    PosMulReflectLT α where elim _a _b _c := lt_of_mul_lt_mul_left'
Strict Order Reflection by Positive Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
For any linearly ordered commutative group with zero $\alpha$, multiplication by a positive element reflects the strict order: if $b \cdot a_1 < b \cdot a_2$ for some positive $b$, then $a_1 < a_2$.
LinearOrderedCommGroupWithZero.toPosMulStrictMono instance
: PosMulStrictMono α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toPosMulStrictMono :
    PosMulStrictMono α where
  elim a b c hbc := by dsimp only; by_contra! h; exact hbc.not_le <| (mul_le_mul_left a.2).1 h
Strict Monotonicity of Left Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
For any linearly ordered commutative group with zero $\alpha$, left multiplication by positive elements is strictly monotone. That is, for any positive element $b > 0$ and any elements $a_1, a_2 \in \alpha$, if $a_1 < a_2$, then $b \cdot a_1 < b \cdot a_2$.
LinearOrderedCommGroupWithZero.toMulPosStrictMono instance
: MulPosStrictMono α
Full source 
instance (priority := 100) LinearOrderedCommGroupWithZero.toMulPosStrictMono :
    MulPosStrictMono α where
  elim a b c hbc := by dsimp only; by_contra! h; exact hbc.not_le <| (mul_le_mul_right a.2).1 h
Strict Monotonicity of Right Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
Every linearly ordered commutative group with zero $\alpha$ satisfies the property that right multiplication by a positive element is strictly monotone. That is, for any positive element $b > 0$ in $\alpha$, if $a_1 < a_2$, then $a_1 * b < a_2 * b$.
mul_inv_le_of_le_mul theorem
(hab : a ≤ b * c) : a * c⁻¹ ≤ b
Full source 
@[deprecated mul_inv_le_of_le_mul₀ (since := "2024-11-18")]
theorem mul_inv_le_of_le_mul (hab : a ≤ b * c) : a * c⁻¹ ≤ b :=
  mul_inv_le_of_le_mul₀ zero_le' zero_le' hab
Inequality for Multiplication by Inverse: $a \leq b \cdot c$ implies $a \cdot c^{-1} \leq b$
Informal description
For any elements $a$, $b$, and $c$ in a linearly ordered commutative group with zero, if $a \leq b \cdot c$, then $a \cdot c^{-1} \leq b$.
Units.zero_lt theorem
(u : αˣ) : (0 : α) < u
Full source 
@[simp]
theorem Units.zero_lt (u : αˣ) : (0 : α) < u :=
  zero_lt_iff.2 u.ne_zero
Invertible Elements are Positive in Linearly Ordered Commutative Groups with Zero
Informal description
For any invertible element $u$ in a linearly ordered commutative group with zero $\alpha$, the zero element is strictly less than $u$, i.e., $0 < u$.
mul_lt_mul_of_lt_of_le₀ theorem
(hab : a ≤ b) (hb : b ≠ 0) (hcd : c < d) : a * c < b * d
Full source 
@[deprecated mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (since := "2024-11-18")]
theorem mul_lt_mul_of_lt_of_le₀ (hab : a ≤ b) (hb : b ≠ 0) (hcd : c < d) : a * c < b * d :=
  mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hab hcd zero_le' (zero_lt_iff.2 hb)
Strict Inequality under Multiplication in Linearly Ordered Commutative Groups with Zero: $a \leq b \land b \neq 0 \land c < d \implies a \cdot c < b \cdot d$
Informal description
Let $\alpha$ be a linearly ordered commutative group with zero. For any elements $a, b, c, d \in \alpha$ such that $a \leq b$, $b \neq 0$, and $c < d$, we have $a \cdot c < b \cdot d$.
mul_lt_mul₀ theorem
(hab : a < b) (hcd : c < d) : a * c < b * d
Full source 
@[deprecated mul_lt_mul'' (since := "2024-11-18")]
theorem mul_lt_mul₀ (hab : a < b) (hcd : c < d) : a * c < b * d :=
  mul_lt_mul'' hab hcd zero_le' zero_le'
Strict Inequality Preservation under Multiplication in Linearly Ordered Commutative Groups with Zero
Informal description
For any elements $a, b, c, d$ in a linearly ordered commutative group with zero $\alpha$, if $a < b$ and $c < d$, then $a \cdot c < b \cdot d$.
mul_inv_lt_of_lt_mul₀ theorem
(h : a < b * c) : a * c⁻¹ < b
Full source 
theorem mul_inv_lt_of_lt_mul₀ (h : a < b * c) : a * c⁻¹ < b := by
  contrapose! h
  simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le' zero_le' h
Inequality for Multiplication by Inverse: $a < b \cdot c$ implies $a \cdot c^{-1} < b$
Informal description
For any elements $a$, $b$, and $c$ in a linearly ordered commutative group with zero, if $a < b \cdot c$, then $a \cdot c^{-1} < b$.
inv_mul_lt_of_lt_mul₀ theorem
(h : a < b * c) : b⁻¹ * a < c
Full source 
theorem inv_mul_lt_of_lt_mul₀ (h : a < b * c) : b⁻¹ * a < c := by
  rw [mul_comm] at *
  exact mul_inv_lt_of_lt_mul₀ h
Inequality for Inverse Multiplication: $a < b \cdot c$ implies $b^{-1} \cdot a < c$
Informal description
For any elements $a$, $b$, and $c$ in a linearly ordered commutative group with zero, if $a < b \cdot c$, then $b^{-1} \cdot a < c$.
lt_of_mul_lt_mul_of_le₀ theorem
(h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d
Full source 
theorem lt_of_mul_lt_mul_of_le₀ (h : a * b < c * d) (hc : 0 < c) (hh : c ≤ a) : b < d := by
  have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
  rw [← inv_le_inv₀ (zero_lt_iff.2 ha) hc] at hh
  simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ hc.ne']
    using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos hh  h zero_le' (inv_pos.2 hc)
Inequality Preservation under Multiplication: $a \cdot b < c \cdot d \land 0 < c \land c \leq a \implies b < d$
Informal description
For any elements $a, b, c, d$ in a linearly ordered commutative group with zero, if $a \cdot b < c \cdot d$, $0 < c$, and $c \leq a$, then $b < d$.
div_le_div_right₀ theorem
(hc : c ≠ 0) : a / c ≤ b / c ↔ a ≤ b
Full source 
@[deprecated div_le_div_iff_of_pos_right (since := "2024-11-18")]
theorem div_le_div_right₀ (hc : c ≠ 0) : a / c ≤ b / c ↔ a ≤ b :=
  div_le_div_iff_of_pos_right (zero_lt_iff.2 hc)
Division Preserves Order for Nonzero Elements: $\frac{a}{c} \leq \frac{b}{c} \leftrightarrow a \leq b$
Informal description
For any nonzero element $c$ in a linearly ordered commutative group with zero, the inequality $\frac{a}{c} \leq \frac{b}{c}$ holds if and only if $a \leq b$.
div_le_div_left₀ theorem
(ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : a / b ≤ a / c ↔ c ≤ b
Full source 
@[deprecated div_le_div_iff_of_pos_left (since := "2024-11-18")]
theorem div_le_div_left₀ (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : a / b ≤ a / c ↔ c ≤ b :=
  div_le_div_iff_of_pos_left (zero_lt_iff.2 ha) (zero_lt_iff.2 hb) (zero_lt_iff.2 hc)
Division Inequality for Nonzero Elements: $\frac{a}{b} \leq \frac{a}{c} \leftrightarrow c \leq b$ when $a, b, c \neq 0$
Informal description
For any nonzero elements $a, b, c$ in a linearly ordered commutative group with zero, the inequality $\frac{a}{b} \leq \frac{a}{c}$ holds if and only if $c \leq b$.
OrderIso.mulLeft₀' definition
{a : α} (ha : a ≠ 0) : α ≃o α
Full source 
/-- `Equiv.mulLeft₀` as an `OrderIso` on a `LinearOrderedCommGroupWithZero.`. -/
@[simps! +simpRhs apply toEquiv,
deprecated OrderIso.mulLeft₀ (since := "2024-11-18")]
def OrderIso.mulLeft₀' {a : α} (ha : a ≠ 0) : α ≃o α := .mulLeft₀ a (zero_lt_iff.2 ha)
Order isomorphism induced by left multiplication with a nonzero element
Informal description
For a linearly ordered commutative group with zero $\alpha$ and a nonzero element $a \in \alpha$, the function $x \mapsto a \cdot x$ is an order isomorphism from $\alpha$ to itself. That is, it is a bijective map that preserves the order relation: for any $x, y \in \alpha$, $x \leq y$ if and only if $a \cdot x \leq a \cdot y$.
OrderIso.mulLeft₀'_symm theorem
{a : α} (ha : a ≠ 0) : (OrderIso.mulLeft₀' ha).symm = OrderIso.mulLeft₀' (inv_ne_zero ha)
Full source 
@[deprecated OrderIso.mulLeft₀_symm (since := "2024-11-18")]
theorem OrderIso.mulLeft₀'_symm {a : α} (ha : a ≠ 0) :
    (OrderIso.mulLeft₀' ha).symm = OrderIso.mulLeft₀' (inv_ne_zero ha) := by
  ext
  rfl
Inverse of Left Multiplication by Nonzero Element in Ordered Group with Zero: $(x \mapsto a \cdot x)^{-1} = (x \mapsto a^{-1} \cdot x)$
Informal description
For any nonzero element $a$ in a linearly ordered commutative group with zero $\alpha$, the inverse of the order isomorphism $x \mapsto a \cdot x$ is equal to the order isomorphism $x \mapsto a^{-1} \cdot x$, where $a^{-1}$ is the multiplicative inverse of $a$.
OrderIso.mulRight₀' definition
{a : α} (ha : a ≠ 0) : α ≃o α
Full source 
/-- `Equiv.mulRight₀` as an `OrderIso` on a `LinearOrderedCommGroupWithZero.`. -/
@[simps! +simpRhs apply toEquiv,
deprecated OrderIso.mulRight₀ (since := "2024-11-18")]
def OrderIso.mulRight₀' {a : α} (ha : a ≠ 0) : α ≃o α := .mulRight₀ a (zero_lt_iff.2 ha)
Order isomorphism induced by right multiplication with a nonzero element
Informal description
For a linearly ordered commutative group with zero $\alpha$ and a nonzero element $a \in \alpha$, the function $x \mapsto x * a$ is an order isomorphism from $\alpha$ to itself. This means it is a bijective map that preserves the order relation: for any $x, y \in \alpha$, $x \leq y$ if and only if $x * a \leq y * a$.
OrderIso.mulRight₀'_symm theorem
{a : α} (ha : a ≠ 0) : (OrderIso.mulRight₀' ha).symm = OrderIso.mulRight₀' (inv_ne_zero ha)
Full source 
@[deprecated OrderIso.mulRight₀_symm (since := "2024-11-18")]
theorem OrderIso.mulRight₀'_symm {a : α} (ha : a ≠ 0) :
    (OrderIso.mulRight₀' ha).symm = OrderIso.mulRight₀' (inv_ne_zero ha) := by
  ext
  rfl
Inverse of Right Multiplication by Nonzero Element in Ordered Group with Zero
Informal description
For any nonzero element $a$ in a linearly ordered commutative group with zero $\alpha$, the inverse of the order isomorphism $x \mapsto x * a$ is equal to the order isomorphism $x \mapsto x * a^{-1}$, where $a^{-1}$ is the multiplicative inverse of $a$.
instLinearOrderedAddCommGroupWithTopAdditiveOrderDual instance
: LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ)
Full source 
instance : LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ) where
  neg_top := inv_zero (G₀ := α)
  add_neg_cancel := fun a ha ↦ mul_inv_cancel₀ (G₀ := α) (id ha : a.toMul ≠ 0)
Additive Order Dual of a Linearly Ordered Commutative Group with Zero is a Linearly Ordered Commutative Additive Group with Top
Informal description
For any linearly ordered commutative group with zero $\alpha$, the additive monoid of its order dual $\alpha^{\text{op}}$ is a linearly ordered commutative additive group with top.
instLinearOrderedAddCommGroupWithTopOrderDualAdditive instance
: LinearOrderedAddCommGroupWithTop (Additive α)ᵒᵈ
Full source 
instance : LinearOrderedAddCommGroupWithTop (Additive α)ᵒᵈ where
  neg_top := inv_zero (G₀ := α)
  add_neg_cancel := fun a ha ↦ mul_inv_cancel₀ (G₀ := α) (id ha : a.toMul ≠ 0)
Order Dual of Additive Monoid as Linearly Ordered Commutative Additive Group with Top
Informal description
The order dual of the additive monoid of a linearly ordered commutative group with top is itself a linearly ordered commutative additive group with top.
pow_lt_pow_succ theorem
(ha : 1 < a) : a ^ n < a ^ n.succ
Full source 
@[deprecated pow_lt_pow_right₀ (since := "2024-11-18")]
lemma pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := pow_lt_pow_right₀ ha n.lt_succ_self
Strict Monotonicity of Successive Powers: $a^n < a^{n+1}$ for $a > 1$
Informal description
For any element $a > 1$ in a linearly ordered commutative group with zero and any natural number $n$, we have $a^n < a^{n+1}$.
instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual instance
[LinearOrderedAddCommMonoidWithTop α] : LinearOrderedCommMonoidWithZero (Multiplicative αᵒᵈ)
Full source 
instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual
    [LinearOrderedAddCommMonoidWithTop α] :
    LinearOrderedCommMonoidWithZero (Multiplicative αᵒᵈ) where
  zero := Multiplicative.ofAdd (OrderDual.toDual ⊤)
  zero_mul := @top_add _ (_)
  -- Porting note:  Here and elsewhere in the file, just `zero_mul` worked in Lean 3. See
  -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonyms
  mul_zero := @add_top _ (_)
  zero_le_one := (le_top : (0 : α) ≤ ⊤)
Multiplicative Order Dual of a Linearly Ordered Additive Monoid with Top is a Linearly Ordered Commutative Monoid with Zero
Informal description
For any linearly ordered commutative additive monoid with top element $\alpha$, the multiplicative order dual $\text{Multiplicative}(\alpha^{\text{op}})$ is a linearly ordered commutative monoid with zero.
ofAdd_toDual_eq_zero_iff theorem
[LinearOrderedAddCommMonoidWithTop α] (x : α) : Multiplicative.ofAdd (OrderDual.toDual x) = 0 ↔ x = ⊤
Full source 
@[simp]
theorem ofAdd_toDual_eq_zero_iff [LinearOrderedAddCommMonoidWithTop α]
    (x : α) : Multiplicative.ofAddMultiplicative.ofAdd (OrderDual.toDual x) = 0 ↔ x = ⊤ := Iff.rfl
Characterization of Zero in Multiplicative Order Dual via Top Element
Informal description
Let $\alpha$ be a linearly ordered commutative additive monoid with a top element $\top$. For any element $x \in \alpha$, the equivalence $\text{Multiplicative.ofAdd}(\text{OrderDual.toDual}(x)) = 0$ holds if and only if $x = \top$.
ofDual_toAdd_eq_top_iff theorem
[LinearOrderedAddCommMonoidWithTop α] (x : Multiplicative αᵒᵈ) : OrderDual.ofDual x.toAdd = ⊤ ↔ x = 0
Full source 
@[simp]
theorem ofDual_toAdd_eq_top_iff [LinearOrderedAddCommMonoidWithTop α]
    (x : Multiplicative αᵒᵈ) : OrderDual.ofDualOrderDual.ofDual x.toAdd = ⊤ ↔ x = 0 := Iff.rfl
Characterization of Zero in Multiplicative Order Dual via Top Element
Informal description
Let $\alpha$ be a linearly ordered commutative additive monoid with a top element $\top$. For any element $x$ in the multiplicative order dual of $\alpha$, the following equivalence holds: the additive counterpart of $x$ (after removing the order dual) equals $\top$ if and only if $x$ is the zero element of the multiplicative monoid. In symbols: $$\text{ofDual}(\text{toAdd}(x)) = \top \leftrightarrow x = 0$$
ofAdd_bot theorem
[LinearOrderedAddCommMonoidWithTop α] : Multiplicative.ofAdd ⊥ = (0 : Multiplicative αᵒᵈ)
Full source 
@[simp]
theorem ofAdd_bot [LinearOrderedAddCommMonoidWithTop α] :
    Multiplicative.ofAdd ⊥ = (0 : Multiplicative αᵒᵈ) := rfl
Bottom Element Maps to Zero in Multiplicative Order Dual
Informal description
For any linearly ordered commutative additive monoid $\alpha$ with a top element $\top$, the image of the bottom element $\bot$ under the multiplicative equivalence `Multiplicative.ofAdd` is equal to the zero element of the multiplicative order dual $\text{Multiplicative}(\alpha^{\text{op}})$.
ofDual_toAdd_zero theorem
[LinearOrderedAddCommMonoidWithTop α] : OrderDual.ofDual (0 : Multiplicative αᵒᵈ).toAdd = ⊤
Full source 
@[simp]
theorem ofDual_toAdd_zero [LinearOrderedAddCommMonoidWithTop α] :
    OrderDual.ofDual (0 : Multiplicative αᵒᵈ).toAdd = ⊤ := rfl
Zero in Multiplicative Order Dual Maps to Top Element
Informal description
Let $\alpha$ be a linearly ordered commutative additive monoid with a top element $\top$. Then, the order dual of the additive representation of the zero element in the multiplicative order dual of $\alpha$ is equal to $\top$. That is, $\text{ofDual}(\text{toAdd}(0)) = \top$.
instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop instance
[LinearOrderedAddCommGroupWithTop α] : LinearOrderedCommGroupWithZero (Multiplicative αᵒᵈ)
Full source 
instance [LinearOrderedAddCommGroupWithTop α] :
    LinearOrderedCommGroupWithZero (Multiplicative αᵒᵈ) :=
  { Multiplicative.divInvMonoid, instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual,
    Multiplicative.instNontrivial with
    inv_zero := @LinearOrderedAddCommGroupWithTop.neg_top _ (_)
    mul_inv_cancel := @LinearOrderedAddCommGroupWithTop.add_neg_cancel _ (_) }
Multiplicative Order Dual of a Linearly Ordered Additive Group with Top is a Linearly Ordered Commutative Group with Zero
Informal description
For any linearly ordered commutative additive group with top element $\alpha$, the multiplicative order dual $\text{Multiplicative}(\alpha^{\text{op}})$ is a linearly ordered commutative group with zero.
WithZero.instPreorder instance
: Preorder (WithZero α)
Full source 
instance instPreorder : Preorder (WithZero α) := WithBot.preorder
Preorder Structure on Type with Zero Adjoined
Informal description
For any type $\alpha$, the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$) has a canonical preorder structure where $0 \leq a$ for all $a \in \alpha \cup \{0\}$.
WithZero.instOrderBot instance
: OrderBot (WithZero α)
Full source 
instance instOrderBot : OrderBot (WithZero α) := WithBot.orderBot
Bottom Element in the Order of a Type with Zero Adjoined
Informal description
For any type $\alpha$, the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$) has a bottom element $0$ in its order structure, meaning $0 \leq a$ for all $a \in \alpha \cup \{0\}$.
WithZero.zero_le theorem
(a : WithZero α) : 0 ≤ a
Full source 
lemma zero_le (a : WithZero α) : 0 ≤ a := bot_le
Zero is Least Element in Type with Zero Adjoined
Informal description
For any element $a$ in the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$), the zero element is less than or equal to $a$, i.e., $0 \leq a$.
WithZero.zero_lt_coe theorem
(a : α) : (0 : WithZero α) < a
Full source 
lemma zero_lt_coe (a : α) : (0 : WithZero α) < a := WithBot.bot_lt_coe a
Zero is Less Than Any Nonzero Element in Type with Zero Adjoined
Informal description
For any element $a$ of a type $\alpha$, the zero element in $\alpha \cup \{0\}$ is strictly less than $a$ (viewed as an element of $\alpha \cup \{0\}$), i.e., $0 < a$.
WithZero.zero_eq_bot theorem
: (0 : WithZero α) = ⊥
Full source 
lemma zero_eq_bot : (0 : WithZero α) = ⊥ := rfl
Zero Equals Bottom in Type with Zero Adjoined
Informal description
In the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$), the zero element is equal to the bottom element of the order structure, i.e., $0 = \bot$.
WithZero.coe_lt_coe theorem
: (a : WithZero α) < b ↔ a < b
Full source 
@[simp, norm_cast] lemma coe_lt_coe : (a : WithZero α) < b ↔ a < b := WithBot.coe_lt_coe
Preservation of Strict Inequality in Type with Zero Adjoined
Informal description
For any two elements $a$ and $b$ of a type $\alpha$ with a zero element adjoined, the inequality $a < b$ holds in $\alpha \cup \{0\}$ if and only if it holds in $\alpha$.
WithZero.coe_le_coe theorem
: (a : WithZero α) ≤ b ↔ a ≤ b
Full source 
@[simp, norm_cast] lemma coe_le_coe : (a : WithZero α) ≤ b ↔ a ≤ b := WithBot.coe_le_coe
Preservation of Inequality in Type with Zero Adjoined
Informal description
For any two elements $a$ and $b$ in a type $\alpha$ with a zero element adjoined, the inequality $a \leq b$ holds in $\alpha \cup \{0\}$ if and only if $a \leq b$ holds in $\alpha$.
WithZero.one_lt_coe theorem
[One α] : 1 < (a : WithZero α) ↔ 1 < a
Full source 
@[simp, norm_cast] lemma one_lt_coe [One α] : 1 < (a : WithZero α) ↔ 1 < a := coe_lt_coe
Preservation of Strict Inequality Against One in Type with Zero Adjoined
Informal description
For any element $a$ in a type $\alpha$ with a multiplicative identity, the inequality $1 < a$ holds in $\alpha \cup \{0\}$ if and only if $1 < a$ holds in $\alpha$.
WithZero.one_le_coe theorem
[One α] : 1 ≤ (a : WithZero α) ↔ 1 ≤ a
Full source 
@[simp, norm_cast] lemma one_le_coe [One α] : 1 ≤ (a : WithZero α) ↔ 1 ≤ a := coe_le_coe
Preservation of Inequality Against One in Type with Zero Adjoined
Informal description
For any element $a$ in a type $\alpha$ with a multiplicative identity, the inequality $1 \leq a$ holds in $\alpha \cup \{0\}$ if and only if $1 \leq a$ holds in $\alpha$.
WithZero.coe_lt_one theorem
[One α] : (a : WithZero α) < 1 ↔ a < 1
Full source 
@[simp, norm_cast] lemma coe_lt_one [One α] : (a : WithZero α) < 1 ↔ a < 1 := coe_lt_coe
Preservation of Strict Inequality Against One in Type with Zero Adjoined
Informal description
For any element $a$ in $\alpha \cup \{0\}$ where $\alpha$ has a multiplicative identity, $a < 1$ holds in $\alpha \cup \{0\}$ if and only if $a < 1$ holds in $\alpha$.
WithZero.coe_le_one theorem
[One α] : (a : WithZero α) ≤ 1 ↔ a ≤ 1
Full source 
@[simp, norm_cast] lemma coe_le_one [One α] : (a : WithZero α) ≤ 1 ↔ a ≤ 1 := coe_le_coe
Preservation of Inequality Against One in Type with Zero Adjoined
Informal description
For any element $a$ in $\alpha \cup \{0\}$ where $\alpha$ has a multiplicative identity, the inequality $a \leq 1$ holds in $\alpha \cup \{0\}$ if and only if $a \leq 1$ holds in $\alpha$.
WithZero.coe_le_iff theorem
{x : WithZero α} : (a : WithZero α) ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b
Full source 
theorem coe_le_iff {x : WithZero α} : (a : WithZero α) ≤ x ↔ ∃ b : α, x = b ∧ a ≤ b :=
  WithBot.coe_le_iff
Characterization of Order Relation in Type with Zero Adjoined
Informal description
For any element $a$ in $\alpha \cup \{0\}$ and any element $x$ in $\alpha \cup \{0\}$, $a \leq x$ holds if and only if there exists an element $b \in \alpha$ such that $x = b$ and $a \leq b$.
WithZero.unzero_le_unzero theorem
{a b : WithZero α} (ha hb) : unzero (x := a) ha ≤ unzero (x := b) hb ↔ a ≤ b
Full source 
@[simp] lemma unzero_le_unzero {a b : WithZero α} (ha hb) :
    unzerounzero (x := a) ha ≤ unzero (x := b) hb ↔ a ≤ b := by
  -- TODO: Fix `lift` so that it doesn't try to clear the hypotheses I give it when it is
  -- impossible to do so. See https://github.com/leanprover-community/mathlib4/issues/19160
  lift a to α using id ha
  lift b to α using id hb
  simp
Order Preservation of Unzero Operation in Type with Zero Adjoined
Informal description
For any elements $a$ and $b$ in $\alpha \cup \{0\}$ that are nonzero (with proofs $ha$ and $hb$ respectively), the inequality $\text{unzero}(a, ha) \leq \text{unzero}(b, hb)$ holds if and only if $a \leq b$ in $\alpha \cup \{0\}$.
WithZero.instMulLeftMono instance
[Mul α] [MulLeftMono α] : MulLeftMono (WithZero α)
Full source 
instance instMulLeftMono [Mul α] [MulLeftMono α] :
    MulLeftMono (WithZero α) := by
  refine ⟨fun a b c hbc => ?_⟩
  induction a; · exact zero_le _
  induction b; · exact zero_le _
  rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
  rw [← coe_mul _ c, ← coe_mul, coe_le_coe]
  exact mul_le_mul_left' hbc' _
Left Monotonicity of Multiplication in Type with Zero Adjoined
Informal description
For any type $\alpha$ with a multiplication operation that is left-monotone (i.e., $a \leq b$ implies $c * a \leq c * b$ for all $c \in \alpha$), the type $\alpha$ with a zero element adjoined also has a left-monotone multiplication operation.
WithZero.addLeftMono theorem
[AddZeroClass α] [AddLeftMono α] (h : ∀ a : α, 0 ≤ a) : AddLeftMono (WithZero α)
Full source 
protected lemma addLeftMono [AddZeroClass α] [AddLeftMono α]
    (h : ∀ a : α, 0 ≤ a) : AddLeftMono (WithZero α) := by
  refine ⟨fun a b c hbc => ?_⟩
  induction a
  · rwa [zero_add, zero_add]
  induction b
  · rw [add_zero]
    induction c
    · rw [add_zero]
    · rw [← coe_add, coe_le_coe]
      exact le_add_of_nonneg_right (h _)
  · rcases WithZero.coe_le_iff.1 hbc with ⟨c, rfl, hbc'⟩
    rw [← coe_add, ← coe_add _ c, coe_le_coe]
    exact add_le_add_left hbc' _
Left Monotonicity of Addition in Type with Zero Adjoined
Informal description
Let $\alpha$ be a type with an addition operation and a zero element (i.e., an `AddZeroClass`), and suppose that addition is left-monotone on $\alpha$ (i.e., $a \leq b$ implies $c + a \leq c + b$ for all $c \in \alpha$). If every element of $\alpha$ is non-negative (i.e., $0 \leq a$ for all $a \in \alpha$), then addition is also left-monotone on $\alpha \cup \{0\}$ (the type $\alpha$ with a zero element adjoined).
WithZero.instExistsAddOfLE instance
[Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithZero α)
Full source 
instance instExistsAddOfLE [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithZero α) :=
  ⟨fun {a b} => by
    induction a
    · exact fun _ => ⟨b, (zero_add b).symm⟩
    induction b
    · exact fun h => (WithBot.not_coe_le_bot _ h).elim
    intro h
    obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)
    exact ⟨c, rfl⟩⟩
Existence of Additive Differences in Type with Zero Adjoined
Informal description
For any type $\alpha$ with an addition operation and the property that for any $a \leq b$ there exists $c$ such that $a + c = b$, the type $\alpha$ with a zero element adjoined also has this property.
WithZero.instPartialOrder instance
: PartialOrder (WithZero α)
Full source 
instance instPartialOrder : PartialOrder (WithZero α) := WithBot.partialOrder
Partial Order on Type with Zero Adjoined
Informal description
For any type $\alpha$, the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$) has a canonical partial order structure.
WithZero.instMulLeftReflectLT instance
[Mul α] [MulLeftReflectLT α] : MulLeftReflectLT (WithZero α)
Full source 
instance instMulLeftReflectLT [Mul α] [MulLeftReflectLT α] :
    MulLeftReflectLT (WithZero α) := by
  refine ⟨fun a b c h => ?_⟩
  have := ((zero_le _).trans_lt h).ne'
  induction a
  · simp at this
  induction c
  · simp at this
  induction b
  exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]
Left Multiplication Reflects Strict Inequalities in Type with Zero Adjoined
Informal description
For any type $\alpha$ with a multiplication operation and the property that left multiplication reflects strict inequalities (i.e., $c \cdot a < c \cdot b$ implies $a < b$ for all $c \neq 0$), the type $\alpha$ with a zero element adjoined also has this property.
WithZero.instLattice instance
[Lattice α] : Lattice (WithZero α)
Full source 
instance instLattice [Lattice α] : Lattice (WithZero α) := WithBot.lattice
Lattice Structure on Type with Zero Adjoined
Informal description
For any lattice $\alpha$, the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$) is also a lattice, where the join and meet operations extend those of $\alpha$ with $0$ as the bottom element.
WithZero.instLinearOrder instance
: LinearOrder (WithZero α)
Full source 
instance instLinearOrder : LinearOrder (WithZero α) := WithBot.linearOrder
Linear Order on Adjoined Zero Element
Informal description
For any type $\alpha$, the type `WithZero α` (obtained by adjoining a zero element to $\alpha$) has a canonical linear order structure.
WithZero.le_max_iff theorem
: (a : WithZero α) ≤ max (b : WithZero α) c ↔ a ≤ max b c
Full source 
protected lemma le_max_iff : (a : WithZero α) ≤ max (b : WithZero α) c ↔ a ≤ max b c := by
  simp only [WithZero.coe_le_coe, le_max_iff]
Inequality Characterization for Maximum in Adjoined Zero Type
Informal description
For any elements $a, b, c$ in a type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$), the inequality $a \leq \max(b, c)$ holds if and only if $a \leq \max(b, c)$ in the linear order on $\alpha \cup \{0\}$.
WithZero.min_le_iff theorem
: min (a : WithZero α) b ≤ c ↔ min a b ≤ c
Full source 
protected lemma min_le_iff : minmin (a : WithZero α) b ≤ c ↔ min a b ≤ c := by
  simp only [WithZero.coe_le_coe, min_le_iff]
Minimum Order Relation in Type with Adjoined Zero
Informal description
For any elements $a$, $b$, and $c$ in a type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$), the minimum of $a$ and $b$ is less than or equal to $c$ if and only if the minimum of $a$ and $b$ is less than or equal to $c$.
WithZero.isOrderedMonoid instance
[CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedMonoid (WithZero α)
Full source 
instance isOrderedMonoid [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] :
    IsOrderedMonoid (WithZero α) where
  mul_le_mul_left := fun _ _ => mul_le_mul_left'
Ordered Monoid Structure on Type with Zero Adjoined
Informal description
For any commutative monoid $\alpha$ with a partial order that makes it an ordered monoid, the type $\alpha \cup \{0\}$ (formed by adjoining a zero element to $\alpha$) is also an ordered monoid.
WithZero.isOrderedAddMonoid theorem
[AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (zero_le : ∀ a : α, 0 ≤ a) : IsOrderedAddMonoid (WithZero α)
Full source 
/-- If `0` is the least element in `α`, then `WithZero α` is an ordered `AddMonoid`. -/
-- See note [reducible non-instances]
protected lemma isOrderedAddMonoid [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α]
    (zero_le : ∀ a : α, 0 ≤ a) :
    IsOrderedAddMonoid (WithZero α) where
  add_le_add_left := @add_le_add_left _ _ _ (WithZero.addLeftMono zero_le)
Adjoining Zero Preserves Ordered Additive Monoid Structure
Informal description
Let $\alpha$ be an additive commutative monoid with a partial order such that addition is monotone (i.e., $\alpha$ is an ordered additive monoid). If every element $a \in \alpha$ satisfies $0 \leq a$, then the type $\alpha \cup \{0\}$ (denoted `WithZero α`) is also an ordered additive monoid.
WithZero.instCanonicallyOrderedAdd instance
[AddZeroClass α] [Preorder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedAdd (WithZero α)
Full source 
/-- Adding a new zero to a canonically ordered additive monoid produces another one. -/
instance instCanonicallyOrderedAdd [AddZeroClass α] [Preorder α] [CanonicallyOrderedAdd α] :
    CanonicallyOrderedAdd (WithZero α) :=
  { WithZero.instExistsAddOfLE with
    le_self_add := fun a b => by
      induction a
      · exact bot_le
      induction b
      · exact le_rfl
      · exact WithZero.coe_le_coe.2 le_self_add }
Canonically Ordered Additive Monoid Structure on Type with Zero Adjoined
Informal description
For any type $\alpha$ with an addition operation, a preorder, and the structure of a canonically ordered additive monoid, the type $\alpha$ with a zero element adjoined (denoted $\alpha \cup \{0\}$) is also a canonically ordered additive monoid. This means that the order relation $\leq$ on $\alpha \cup \{0\}$ coincides with the subtractibility relation, i.e., $a \leq b$ if and only if there exists $c$ such that $b = a + c$.
WithZero.instLinearOrderedCommMonoidWithZero instance
[CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] : LinearOrderedCommMonoidWithZero (WithZero α)
Full source 
instance instLinearOrderedCommMonoidWithZero [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] :
    LinearOrderedCommMonoidWithZero (WithZero α) where
  zero_le_one := WithZero.zero_le _
Linearly Ordered Commutative Monoid with Zero from Adjoining Zero to a Linearly Ordered Commutative Monoid
Informal description
For any commutative monoid $\alpha$ with a linear order that is compatible with the monoid operation (i.e., multiplication is monotone in both arguments), the type $\alpha \cup \{0\}$ (obtained by adjoining a zero element to $\alpha$) is a linearly ordered commutative monoid with zero. Here, the order extends the original order on $\alpha$ with $0$ as the least element, and multiplication is extended by $0 \cdot x = x \cdot 0 = 0$ for all $x \in \alpha \cup \{0\}$.
WithZero.instLinearOrderedCommGroupWithZero instance
[CommGroup α] [LinearOrder α] [IsOrderedMonoid α] : LinearOrderedCommGroupWithZero (WithZero α)
Full source 
instance instLinearOrderedCommGroupWithZero [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] :
    LinearOrderedCommGroupWithZero (WithZero α) where
Linearly Ordered Commutative Group with Zero from Adjoining Zero to a Linearly Ordered Commutative Group
Informal description
For any linearly ordered commutative group $\alpha$ where the group operation is compatible with the order (i.e., multiplication is monotone in both arguments), the type $\alpha \cup \{0\}$ (obtained by adjoining a zero element to $\alpha$) is a linearly ordered commutative group with zero. Here, the order extends the original order on $\alpha$ with $0$ as the least element, and multiplication is extended by $0 \cdot x = x \cdot 0 = 0$ for all $x \in \alpha \cup \{0\}$.