Mathlib.Algebra.Order.Group.Basic

zpow_right_strictMono theorem

(ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n

Full source

@[to_additive zsmul_left_strictMono]
lemma zpow_right_strictMono (ha : 1 < a) : StrictMono fun n : ℤ ↦ a ^ n := by
  refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact lt_mul_of_one_lt_right' (a ^ n) ha

Strict Monotonicity of Integer Powers for $a > 1$

Informal description

For any element $a$ in a commutative group $\alpha$ with a partial order, if $1 < a$, then the function $n \mapsto a^n$ is strictly monotone on the integers. That is, for any integers $m < n$, we have $a^m < a^n$.

one_lt_zpow theorem

(ha : 1 < a) (hn : 0 < n) : 1 < a ^ n

Full source

@[to_additive zsmul_pos] lemma one_lt_zpow (ha : 1 < a) (hn : 0 < n) : 1 < a ^ n := by
  simpa using zpow_right_strictMono ha hn

Exponentiation Inequality: $1 < a$ and $0 < n$ implies $1 < a^n$

Informal description

For any element $a$ in a commutative group $\alpha$ with a partial order, if $1 < a$ and $0 < n$ for some integer $n$, then $1 < a^n$.

zpow_right_strictAnti theorem

(ha : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n

Full source

@[to_additive zsmul_left_strictAnti]
lemma zpow_right_strictAnti (ha : a < 1) : StrictAnti fun n : ℤ ↦ a ^ n := by
  refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one]
  exact mul_lt_of_lt_one_right' (a ^ n) ha

Strict Antitonicity of Integer Powers for $a < 1$

Informal description

For any element $a$ in a commutative group $\alpha$ with a partial order, if $a < 1$, then the function $n \mapsto a^n$ is strictly antitone on the integers. That is, for any integers $m < n$, we have $a^n < a^m$.

zpow_right_inj theorem

(ha : 1 < a) {m n : ℤ} : a ^ m = a ^ n ↔ m = n

Full source

@[to_additive zsmul_left_inj]
lemma zpow_right_inj (ha : 1 < a) {m n : ℤ} : a ^ m = a ^ n ↔ m = n :=
  (zpow_right_strictMono ha).injective.eq_iff

Injectivity of Integer Powers for $a > 1$: $a^m = a^n \leftrightarrow m = n$

Informal description

For any element $a$ in a commutative group $\alpha$ with a partial order, if $1 < a$, then for any integers $m$ and $n$, the equality $a^m = a^n$ holds if and only if $m = n$.

zpow_right_mono theorem

(ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n

Full source

@[to_additive zsmul_left_mono]
lemma zpow_right_mono (ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n := by
  refine monotone_int_of_le_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact le_mul_of_one_le_right' ha

Monotonicity of Integer Powers: $1 \leq a$ implies $n \mapsto a^n$ is monotone

Informal description

For any element $a$ in a commutative group $G$ such that $1 \leq a$, the function $n \mapsto a^n$ is monotone with respect to the integer order. That is, for any integers $m \leq n$, we have $a^m \leq a^n$.

zpow_le_zpow_right theorem

(ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n

Full source

@[to_additive (attr := gcongr) zsmul_le_zsmul_left]
lemma zpow_le_zpow_right (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n := zpow_right_mono ha h

Monotonicity of Integer Powers: $a^m \leq a^n$ when $1 \leq a$ and $m \leq n$

Informal description

Let $G$ be a commutative group with a partial order such that $1 \leq a$ for some $a \in G$. Then for any integers $m \leq n$, we have $a^m \leq a^n$.

zpow_lt_zpow_right theorem

(ha : 1 < a) (h : m < n) : a ^ m < a ^ n

Full source

@[to_additive (attr := gcongr) zsmul_lt_zsmul_left]
lemma zpow_lt_zpow_right (ha : 1 < a) (h : m < n) : a ^ m < a ^ n := zpow_right_strictMono ha h

Strict Monotonicity of Integer Powers for $a > 1$

Informal description

Let $G$ be a commutative group with a partial order such that multiplication is monotone. For any element $a \in G$ with $1 < a$ and any integers $m < n$, we have $a^m < a^n$.

zpow_le_zpow_iff_right theorem

(ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

Full source

@[to_additive zsmul_le_zsmul_iff_left]
lemma zpow_le_zpow_iff_right (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
  (zpow_right_strictMono ha).le_iff_le

Comparison of Integer Powers: $a^m \leq a^n \leftrightarrow m \leq n$ for $a > 1$

Informal description

Let $G$ be a commutative group with a partial order, and let $a \in G$ satisfy $1 < a$. Then for any integers $m$ and $n$, we have $a^m \leq a^n$ if and only if $m \leq n$.

zpow_lt_zpow_iff_right theorem

(ha : 1 < a) : a ^ m < a ^ n ↔ m < n

Full source

@[to_additive zsmul_lt_zsmul_iff_left]
lemma zpow_lt_zpow_iff_right (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
  (zpow_right_strictMono ha).lt_iff_lt

Comparison of Integer Powers: $a^m < a^n \leftrightarrow m < n$ for $a > 1$

Informal description

Let $G$ be a commutative group with a partial order, and let $a \in G$ satisfy $1 < a$. Then for any integers $m$ and $n$, we have $a^m < a^n$ if and only if $m < n$.

zpow_left_strictMono theorem

(hn : 0 < n) : StrictMono ((· ^ n) : α → α)

Full source

@[to_additive zsmul_strictMono_right]
lemma zpow_left_strictMono (hn : 0 < n) : StrictMono ((· ^ n) : α → α) := fun a b hab => by
  rw [← one_lt_div', ← div_zpow]; exact one_lt_zpow (one_lt_div'.2 hab) hn

Strict Monotonicity of Integer Powers with Positive Exponents: $a < b \implies a^n < b^n$ for $n > 0$

Informal description

For any integer $n > 0$, the function $x \mapsto x^n$ is strictly monotone on an ordered commutative group $\alpha$. That is, for any $a, b \in \alpha$, if $a < b$, then $a^n < b^n$.

zpow_left_mono theorem

(hn : 0 ≤ n) : Monotone ((· ^ n) : α → α)

Full source

@[to_additive zsmul_mono_right]
lemma zpow_left_mono (hn : 0 ≤ n) : Monotone ((· ^ n) : α → α) := fun a b hab => by
  rw [← one_le_div', ← div_zpow]; exact one_le_zpow (one_le_div'.2 hab) hn

Monotonicity of Integer Powers with Nonnegative Exponents: $a \leq b \implies a^n \leq b^n$ for $n \geq 0$

Informal description

For any element $n$ in an ordered commutative group $\alpha$ such that $0 \leq n$, the function $x \mapsto x^n$ is monotone. That is, for any $a, b \in \alpha$, if $a \leq b$, then $a^n \leq b^n$.

zpow_le_zpow_left theorem

(hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n

Full source

@[to_additive (attr := gcongr) zsmul_le_zsmul_right]
lemma zpow_le_zpow_left (hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n := zpow_left_mono α hn h

Monotonicity of Integer Powers: $a \leq b \implies a^n \leq b^n$ for $n \geq 0$

Informal description

Let $\alpha$ be an ordered commutative group. For any $a, b \in \alpha$ and any integer $n \geq 0$, if $a \leq b$, then $a^n \leq b^n$.

zpow_lt_zpow_left theorem

(hn : 0 < n) (h : a < b) : a ^ n < b ^ n

Full source

@[to_additive (attr := gcongr) zsmul_lt_zsmul_right]
lemma zpow_lt_zpow_left (hn : 0 < n) (h : a < b) : a ^ n < b ^ n := zpow_left_strictMono α hn h

Strict Monotonicity of Integer Powers: $a < b \implies a^n < b^n$ for $n > 0$

Informal description

For any elements $a$ and $b$ in an ordered commutative group $\alpha$ and any positive integer $n$, if $a < b$, then $a^n < b^n$.

zpow_le_zpow_iff_left theorem

(hn : 0 < n) : a ^ n ≤ b ^ n ↔ a ≤ b

Full source

@[to_additive zsmul_le_zsmul_iff_right]
lemma zpow_le_zpow_iff_left (hn : 0 < n) : a ^ n ≤ b ^ n ↔ a ≤ b :=
  (zpow_left_strictMono α hn).le_iff_le

Order-Preserving Property of Integer Powers: $a^n \leq b^n \leftrightarrow a \leq b$ for $n > 0$

Informal description

For any elements $a$ and $b$ in an ordered commutative group $\alpha$ and any positive integer $n$, the inequality $a^n \leq b^n$ holds if and only if $a \leq b$.

zpow_lt_zpow_iff_left theorem

(hn : 0 < n) : a ^ n < b ^ n ↔ a < b

Full source

@[to_additive zsmul_lt_zsmul_iff_right]
lemma zpow_lt_zpow_iff_left (hn : 0 < n) : a ^ n < b ^ n ↔ a < b :=
  (zpow_left_strictMono α hn).lt_iff_lt

Strict Order-Preserving Property of Integer Powers: $a^n < b^n \leftrightarrow a < b$ for $n > 0$

Informal description

For any elements $a$ and $b$ in an ordered commutative group $\alpha$ and any positive integer $n$, the inequality $a^n < b^n$ holds if and only if $a < b$.

instIsMulTorsionFree instance

: IsMulTorsionFree α

Full source

@[to_additive]
instance : IsMulTorsionFree α where pow_left_injective _ hn := (pow_left_strictMono hn).injective

Ordered Commutative Groups are Multiplicatively Torsion-Free

Informal description

Every ordered commutative group $\alpha$ is multiplicatively torsion-free. That is, for any nonzero natural number $n$, the $n$-th power function $a \mapsto a^n$ is injective on $\alpha$. Equivalently, for any $a, b \in \alpha$ and nonzero $n$, we have $a^n = b^n$ if and only if $a = b$.

not_isCyclic_of_denselyOrdered theorem

[DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α

Full source

/-- A nontrivial densely linear ordered commutative group can't be a cyclic group. -/
@[to_additive
  "A nontrivial densely linear ordered additive commutative group can't be a cyclic group."]
theorem not_isCyclic_of_denselyOrdered [DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α := by
  intro h
  rcases exists_zpow_surjective α with ⟨a, ha⟩
  rcases lt_trichotomy a 1 with hlt | rfl | hlt
  · rcases exists_between hlt with ⟨b, hab, hb⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by omega
    rw [← one_lt_inv'] at hlt
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all
  · rcases exists_ne (1 : α) with ⟨b, hb⟩
    simpa [hb.symm] using ha b
  · rcases exists_between hlt with ⟨b, hb, hba⟩
    rcases ha b with ⟨k, rfl⟩
    suffices 0 < k ∧ k < 1 by omega
    simp_rw [← zpow_lt_zpow_iff_right hlt]
    simp_all

Non-cyclicity of Nontrivial Densely Ordered Commutative Groups

Informal description

Let $\alpha$ be a nontrivial, densely linearly ordered commutative group. Then $\alpha$ cannot be a cyclic group.