Documentation

Mathlib.Algebra.Order.Group.Basic

Lemmas about the interaction of power operations with order #

source
theorem zsmul_pos {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} (ha : 0 < a) (hn : 0 < n) :
0 < n • a
source
theorem one_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} (ha : 1 < a) (hn : 0 < n) :
1 < a ^ n
source
theorem zsmul_strictMono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) :
StrictMono fun (n : ℤ) => n • a
source
theorem zpow_right_strictMono {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) :
StrictMono fun (n : ℤ) => a ^ n
source
theorem zsmul_left_inj {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) {m : ℤ} {n : ℤ} :
m • a = n • a ↔ m = n
source
theorem zpow_right_inj {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) {m : ℤ} {n : ℤ} :
a ^ m = a ^ n ↔ m = n
source
theorem zsmul_mono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 ≤ a) :
Monotone fun (n : ℤ) => n • a
source
theorem zpow_mono_right {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 ≤ a) :
Monotone fun (n : ℤ) => a ^ n
source
theorem zsmul_le_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 ≤ a) (h : m ≤ n) :
m • a ≤ n • a
source
theorem zpow_le_zpow {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 ≤ a) (h : m ≤ n) :
a ^ m ≤ a ^ n
source
theorem zsmul_lt_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) (h : m < n) :
m • a < n • a
source
theorem zpow_lt_zpow {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) (h : m < n) :
a ^ m < a ^ n
source
theorem zsmul_le_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) :
m • a ≤ n • a ↔ m ≤ n
source
theorem zpow_le_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) :
a ^ m ≤ a ^ n ↔ m ≤ n
source
theorem zsmul_lt_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 0 < a) :
m • a < n • a ↔ m < n
source
theorem zpow_lt_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : ℤ} {n : ℤ} {a : α} (ha : 1 < a) :
a ^ m < a ^ n ↔ m < n
source
theorem zsmul_strictMono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 < n) :
StrictMono fun (x : α) => n • x
source
theorem zpow_strictMono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 < n) :
StrictMono fun (x : α) => x ^ n
source
theorem zsmul_mono_right (α : Type u_1) [OrderedAddCommGroup α] {n : ℤ} (hn : 0 ≤ n) :
Monotone fun (x : α) => n • x
source
theorem zpow_mono_left (α : Type u_1) [OrderedCommGroup α] {n : ℤ} (hn : 0 ≤ n) :
Monotone fun (x : α) => x ^ n
source
theorem zsmul_le_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 ≤ n) (h : a ≤ b) :
n • a ≤ n • b
source
theorem zpow_le_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 ≤ n) (h : a ≤ b) :
a ^ n ≤ b ^ n
source
theorem zsmul_lt_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) (h : a < b) :
n • a < n • b
source
theorem zpow_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) (h : a < b) :
a ^ n < b ^ n
source
theorem zsmul_le_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) :
n • a ≤ n • b ↔ a ≤ b
source
theorem zpow_le_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) :
a ^ n ≤ b ^ n ↔ a ≤ b
source
theorem zsmul_lt_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) :
n • a < n • b ↔ a < b
source
theorem zpow_lt_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : 0 < n) :
a ^ n < b ^ n ↔ a < b
source
theorem zsmul_right_injective {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} (hn : n ≠ 0) :
Function.Injective fun (x : α) => n • x

See also smul_right_injective. TODO: provide a NoZeroSMulDivisors instance. We can't do that here because importing that definition would create import cycles.

source
theorem zpow_left_injective {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} (hn : n ≠ 0) :
Function.Injective fun (x : α) => x ^ n
source
theorem zsmul_right_inj {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) :
n • a = n • b ↔ a = b
source
theorem zpow_left_inj {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b
source
theorem zsmul_eq_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) :
n • a = n • b ↔ a = b

Alias of zsmul_right_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

source
theorem zpow_eq_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : ℤ} {a : α} {b : α} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b

Alias of zpow_left_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and zsmul_lt_zsmul_iff'.

source
theorem not_isAddCyclic_of_denselyOrdered (α : Type u_1) [LinearOrderedAddCommGroup α] [DenselyOrdered α] [Nontrivial α] :
¬IsAddCyclic α

A nontrivial densely linear ordered additive commutative group can't be a cyclic group.

source
theorem not_isCyclic_of_denselyOrdered (α : Type u_1) [LinearOrderedCommGroup α] [DenselyOrdered α] [Nontrivial α] :
¬IsCyclic α

A nontrivial densely linear ordered commutative group can't be a cyclic group.