Documentation

Mathlib.Algebra.Order.Group.Basic

Lemmas about the interaction of power operations with order #

theorem zsmul_pos {α : Type u_1} [OrderedAddCommGroup α] {n : } {a : α} (ha : 0 < a) (hn : 0 < n) :
0 < n a
theorem one_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : } {a : α} (ha : 1 < a) (hn : 0 < n) :
1 < a ^ n
theorem zsmul_strictMono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) :
StrictMono fun (n : ) => n a
theorem zpow_right_strictMono {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) :
StrictMono fun (n : ) => a ^ n
theorem zsmul_left_inj {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 < a) {m : } {n : } :
m a = n a m = n
theorem zpow_right_inj {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 < a) {m : } {n : } :
a ^ m = a ^ n m = n
theorem zsmul_mono_left {α : Type u_1} [OrderedAddCommGroup α] {a : α} (ha : 0 a) :
Monotone fun (n : ) => n a
theorem zpow_mono_right {α : Type u_1} [OrderedCommGroup α] {a : α} (ha : 1 a) :
Monotone fun (n : ) => a ^ n
theorem zsmul_le_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 a) (h : m n) :
m a n a
theorem zpow_le_zpow {α : Type u_1} [OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 a) (h : m n) :
a ^ m a ^ n
theorem zsmul_lt_zsmul {α : Type u_1} [OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 < a) (h : m < n) :
m a < n a
theorem zpow_lt_zpow {α : Type u_1} [OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 < a) (h : m < n) :
a ^ m < a ^ n
theorem zsmul_le_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 < a) :
m a n a m n
theorem zpow_le_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 < a) :
a ^ m a ^ n m n
theorem zsmul_lt_zsmul_iff {α : Type u_1} [OrderedAddCommGroup α] {m : } {n : } {a : α} (ha : 0 < a) :
m a < n a m < n
theorem zpow_lt_zpow_iff {α : Type u_1} [OrderedCommGroup α] {m : } {n : } {a : α} (ha : 1 < a) :
a ^ m < a ^ n m < n
theorem zsmul_strictMono_right (α : Type u_1) [OrderedAddCommGroup α] {n : } (hn : 0 < n) :
StrictMono fun (x : α) => n x
theorem zpow_strictMono_left (α : Type u_1) [OrderedCommGroup α] {n : } (hn : 0 < n) :
StrictMono fun (x : α) => x ^ n
theorem zsmul_mono_right (α : Type u_1) [OrderedAddCommGroup α] {n : } (hn : 0 n) :
Monotone fun (x : α) => n x
theorem zpow_mono_left (α : Type u_1) [OrderedCommGroup α] {n : } (hn : 0 n) :
Monotone fun (x : α) => x ^ n
theorem zsmul_le_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : 0 n) (h : a b) :
n a n b
theorem zpow_le_zpow' {α : Type u_1} [OrderedCommGroup α] {n : } {a : α} {b : α} (hn : 0 n) (h : a b) :
a ^ n b ^ n
theorem zsmul_lt_zsmul' {α : Type u_1} [OrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) (h : a < b) :
n a < n b
theorem zpow_lt_zpow' {α : Type u_1} [OrderedCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) (h : a < b) :
a ^ n < b ^ n
theorem zsmul_le_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) :
n a n b a b
theorem zpow_le_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) :
a ^ n b ^ n a b
theorem zsmul_lt_zsmul_iff' {α : Type u_1} [LinearOrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) :
n a < n b a < b
theorem zpow_lt_zpow_iff' {α : Type u_1} [LinearOrderedCommGroup α] {n : } {a : α} {b : α} (hn : 0 < n) :
a ^ n < b ^ n a < b
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.

theorem zpow_left_injective {α : Type u_1} [LinearOrderedCommGroup α] {n : } (hn : n 0) :
Function.Injective fun (x : α) => x ^ n
theorem zsmul_right_inj {α : Type u_1} [LinearOrderedAddCommGroup α] {n : } {a : α} {b : α} (hn : n 0) :
n a = n b a = b
theorem zpow_left_inj {α : Type u_1} [LinearOrderedCommGroup α] {n : } {a : α} {b : α} (hn : n 0) :
a ^ n = b ^ n a = b
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'.

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

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

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