Mathlib.Algebra.Order.Group.Defs

OrderedAddCommGroup structure

(α : Type u) extends AddCommGroup α, PartialOrder α

Full source

/-- An ordered additive commutative group is an additive commutative group
with a partial order in which addition is strictly monotone. -/
@[deprecated "Use `[AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α]` instead."
  (since := "2025-04-10")]
structure OrderedAddCommGroup (α : Type u) extends AddCommGroup α, PartialOrder α where
  /-- Addition is monotone in an ordered additive commutative group. -/
  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b

Ordered additive commutative group

Informal description

An ordered additive commutative group is an additive commutative group $(α, +, 0, -)$ equipped with a partial order $\leq$ such that addition is strictly monotone in both arguments: for any $a, b, c \in α$, if $a \leq b$ then $a + c \leq b + c$ and $c + a \leq c + b$.

OrderedCommGroup structure

(α : Type u) extends CommGroup α, PartialOrder α

Full source

/-- An ordered commutative group is a commutative group
with a partial order in which multiplication is strictly monotone. -/
@[to_additive,
  deprecated "Use `[CommGroup α] [PartialOrder α] [IsOrderedMonoid α]` instead."
  (since := "2025-04-10")]
structure OrderedCommGroup (α : Type u) extends CommGroup α, PartialOrder α where
  /-- Multiplication is monotone in an ordered commutative group. -/
  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b

Ordered commutative group

Informal description

An ordered commutative group is a commutative group $(G, \cdot, 1, \leq)$ equipped with a partial order $\leq$ such that multiplication is strictly monotone in both arguments: for all $x, y, z \in G$, if $x \leq y$ then $x \cdot z \leq y \cdot z$ and $z \cdot x \leq z \cdot y$.

IsOrderedMonoid.toIsOrderedCancelMonoid instance

[CommGroup α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedCancelMonoid α

Full source

@[to_additive IsOrderedAddMonoid.toIsOrderedCancelAddMonoid]
instance (priority := 100) IsOrderedMonoid.toIsOrderedCancelMonoid
    [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedCancelMonoid α where
  le_of_mul_le_mul_left a b c bc := by simpa using mul_le_mul_left' bc a⁻¹
  le_of_mul_le_mul_right a b c bc := by simpa using mul_le_mul_left' bc a⁻¹

Ordered Commutative Groups are Ordered Cancellative Monoids

Informal description

Every ordered commutative group $\alpha$ with a partial order that is compatible with multiplication is also an ordered cancellative monoid.

LinearOrderedAddCommGroup structure

(α : Type u) extends OrderedAddCommGroup α, LinearOrder α

Full source

/-- A linearly ordered additive commutative group is an
additive commutative group with a linear order in which
addition is monotone. -/
@[deprecated "Use `[AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]` instead."
  (since := "2025-04-10")]
structure LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, LinearOrder α

Linearly ordered additive commutative group

Informal description

A linearly ordered additive commutative group is an additive commutative group $\alpha$ equipped with a linear order such that addition is monotone with respect to the order. That is, for any $a, b, c \in \alpha$, if $a \leq b$ then $a + c \leq b + c$.

LinearOrderedCommGroup structure

(α : Type u) extends OrderedCommGroup α, LinearOrder α

Full source

/-- A linearly ordered commutative group is a
commutative group with a linear order in which
multiplication is monotone. -/
@[to_additive,
  deprecated "Use `[CommGroup α] [LinearOrder α] [IsOrderedMonoid α]` instead."
  (since := "2025-04-10")]
structure LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup α, LinearOrder α

Linearly Ordered Commutative Group

Informal description

A linearly ordered commutative group is a commutative group equipped with a linear order such that the group operation is monotone with respect to the order. In other words, for any elements $a, b, c$ in the group, if $a < b$, then $c \cdot a < c \cdot b$.

LinearOrderedCommGroup.mul_lt_mul_left' theorem

(a b : α) (h : a < b) (c : α) : c * a < c * b

Full source

@[to_additive LinearOrderedAddCommGroup.add_lt_add_left]
theorem LinearOrderedCommGroup.mul_lt_mul_left' (a b : α) (h : a < b) (c : α) : c * a < c * b :=
  _root_.mul_lt_mul_left' h c

Left Multiplication Preserves Strict Inequality in Linearly Ordered Commutative Groups

Informal description

Let $\alpha$ be a linearly ordered commutative group. For any elements $a, b \in \alpha$ with $a < b$ and any element $c \in \alpha$, we have $c \cdot a < c \cdot b$.

exists_one_lt' theorem

[Nontrivial α] : ∃ a : α, 1 < a

Full source

@[to_additive exists_zero_lt]
theorem exists_one_lt' [Nontrivial α] : ∃ a : α, 1 < a := by
  obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)
  obtain h|h := hy.lt_or_lt
  · exact ⟨y⁻¹, one_lt_inv'.mpr h⟩
  · exact ⟨y, h⟩

Existence of Element Greater Than One in Nontrivial Linearly Ordered Commutative Group

Informal description

In any nontrivial linearly ordered commutative group $\alpha$, there exists an element $a \in \alpha$ such that $1 < a$.

LinearOrderedCommGroup.to_noMaxOrder instance

[Nontrivial α] : NoMaxOrder α

Full source

@[to_additive]
instance (priority := 100) LinearOrderedCommGroup.to_noMaxOrder [Nontrivial α] : NoMaxOrder α :=
  ⟨by
    obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
    exact fun a => ⟨a * y, lt_mul_of_one_lt_right' a hy⟩⟩

No Maximal Elements in Nontrivial Linearly Ordered Commutative Groups

Informal description

For any nontrivial linearly ordered commutative group $\alpha$, the order on $\alpha$ has no maximal elements.

LinearOrderedCommGroup.to_noMinOrder instance

[Nontrivial α] : NoMinOrder α

Full source

@[to_additive]
instance (priority := 100) LinearOrderedCommGroup.to_noMinOrder [Nontrivial α] : NoMinOrder α :=
  ⟨by
    obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
    exact fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩⟩

No Minimal Elements in Nontrivial Linearly Ordered Commutative Groups

Informal description

Every nontrivial linearly ordered commutative group $\alpha$ has no minimal elements. That is, for any element $a \in \alpha$, there exists another element $x \in \alpha$ such that $x < a$.

inv_le_self_iff theorem

: a⁻¹ ≤ a ↔ 1 ≤ a

Full source

@[to_additive (attr := simp)]
theorem inv_le_self_iff : a⁻¹a⁻¹ ≤ a ↔ 1 ≤ a := by simp [inv_le_iff_one_le_mul']

Inverse Inequality in Linearly Ordered Commutative Groups: $a^{-1} \leq a \leftrightarrow 1 \leq a$

Informal description

For any element $a$ in a linearly ordered commutative group, the inequality $a^{-1} \leq a$ holds if and only if $1 \leq a$.

inv_lt_self_iff theorem

: a⁻¹ < a ↔ 1 < a

Full source

@[to_additive (attr := simp)]
theorem inv_lt_self_iff : a⁻¹a⁻¹ < a ↔ 1 < a := by simp [inv_lt_iff_one_lt_mul]

Inverse Element Comparison: $a^{-1} < a \leftrightarrow 1 < a$

Informal description

For any element $a$ in a linearly ordered commutative group, the inequality $a^{-1} < a$ holds if and only if $1 < a$.

le_inv_self_iff theorem

: a ≤ a⁻¹ ↔ a ≤ 1

Full source

@[to_additive (attr := simp)]
theorem le_inv_self_iff : a ≤ a⁻¹ ↔ a ≤ 1 := by simp [← not_iff_not]

Element Less Than or Equal to Its Inverse if and Only if Less Than or Equal to One

Informal description

For any element $a$ in a linearly ordered commutative group, $a$ is less than or equal to its inverse $a^{-1}$ if and only if $a$ is less than or equal to the identity element $1$.

lt_inv_self_iff theorem

: a < a⁻¹ ↔ a < 1

Full source

@[to_additive (attr := simp)]
theorem lt_inv_self_iff : a < a⁻¹ ↔ a < 1 := by simp [← not_iff_not]

Element Less Than Its Inverse iff Less Than One

Informal description

For any element $a$ in a linearly ordered commutative group, $a$ is less than its inverse $a^{-1}$ if and only if $a$ is less than the identity element $1$.

inv_le_inv' theorem

: a ≤ b → b⁻¹ ≤ a⁻¹

Full source

@[to_additive (attr := gcongr) neg_le_neg]
theorem inv_le_inv' : a ≤ b → b⁻¹ ≤ a⁻¹ :=
  inv_le_inv_iff.mpr

Inverse Inequality: $a \leq b \implies b^{-1} \leq a^{-1}$

Informal description

For any elements $a$ and $b$ in a division monoid $\alpha$, if $a \leq b$, then $b^{-1} \leq a^{-1}$.

inv_lt_inv' theorem

: a < b → b⁻¹ < a⁻¹

Full source

@[to_additive (attr := gcongr) neg_lt_neg]
theorem inv_lt_inv' : a < b → b⁻¹ < a⁻¹ :=
  inv_lt_inv_iff.mpr

Inverse Reverses Strict Inequality: $a < b \Rightarrow b^{-1} < a^{-1}$

Informal description

For any elements $a$ and $b$ in an ordered group, if $a < b$, then $b^{-1} < a^{-1}$.

inv_lt_one_of_one_lt theorem

: 1 < a → a⁻¹ < 1

Full source

@[to_additive]
theorem inv_lt_one_of_one_lt : 1 < a → a⁻¹ < 1 :=
  inv_lt_one_iff_one_lt.mpr

Inverse Inequality in Ordered Groups: $1 < a \Rightarrow a^{-1} < 1$

Informal description

For any element $a$ in a linearly ordered commutative group, if $1 < a$, then $a^{-1} < 1$.

inv_le_one_of_one_le theorem

: 1 ≤ a → a⁻¹ ≤ 1

Full source

@[to_additive]
theorem inv_le_one_of_one_le : 1 ≤ a → a⁻¹ ≤ 1 :=
  inv_le_one'.mpr

Inverse Inequality in Ordered Groups: $1 \leq a \Rightarrow a^{-1} \leq 1$

Informal description

For any element $a$ in a linearly ordered commutative group, if $1 \leq a$, then $a^{-1} \leq 1$.

one_le_inv_of_le_one theorem

: a ≤ 1 → 1 ≤ a⁻¹

Full source

@[to_additive neg_nonneg_of_nonpos]
theorem one_le_inv_of_le_one : a ≤ 1 → 1 ≤ a⁻¹ :=
  one_le_inv'.mpr

Inverse Inequality in Ordered Groups: $a \leq 1 \Rightarrow 1 \leq a^{-1}$

Informal description

For any element $a$ in a linearly ordered commutative group, if $a \leq 1$, then $1 \leq a^{-1}$.

Implementation details