Lemmas about the interaction of power operations with order

theorem zpow_right_strictMono {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} (ha : 1 < a) : StrictMono fun (n : ℤ) => a ^ n

theorem zsmul_left_strictMono {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : 0 < a) : StrictMono fun (n : ℤ) => n • a

theorem zpow_right_strictAnti {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} (ha : a < 1) : StrictAnti fun (n : ℤ) => a ^ n

theorem zsmul_left_strictAnti {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : a < 0) : StrictAnti fun (n : ℤ) => n • a

theorem zpow_right_inj {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} (ha : 1 < a) {m n : ℤ} : a ^ m = a ^ n ↔ m = n

theorem zsmul_left_inj {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : 0 < a) {m n : ℤ} : m • a = n • a ↔ m = n

theorem zpow_right_mono {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} (ha : 1 ≤ a) : Monotone fun (n : ℤ) => a ^ n

theorem zsmul_left_mono {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} (ha : 0 ≤ a) : Monotone fun (n : ℤ) => n • a

theorem zpow_le_zpow_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α} (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n

theorem zsmul_le_zsmul_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 ≤ a) (h : m ≤ n) : m • a ≤ n • a

theorem zpow_lt_zpow_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α} (ha : 1 < a) (h : m < n) : a ^ m < a ^ n

theorem zsmul_lt_zsmul_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 < a) (h : m < n) : m • a < n • a

theorem zpow_le_zpow_iff_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α} (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

theorem zsmul_le_zsmul_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 < a) : m • a ≤ n • a ↔ m ≤ n

theorem zpow_lt_zpow_iff_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {m n : ℤ} {a : α} (ha : 1 < a) : a ^ m < a ^ n ↔ m < n

theorem zsmul_lt_zsmul_iff_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {m n : ℤ} {a : α} (ha : 0 < a) : m • a < n • a ↔ m < n

theorem zpow_left_strictMono (α : Type u_1) [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {n : ℤ} (hn : 0 < n) : StrictMono fun (x : α) => x ^ n

theorem zsmul_strictMono_right (α : Type u_1) [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} (hn : 0 < n) : StrictMono fun (x : α) => n • x

theorem zpow_left_mono (α : Type u_1) [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun (x : α) => x ^ n

theorem zsmul_mono_right (α : Type u_1) [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} (hn : 0 ≤ n) : Monotone fun (x : α) => n • x

theorem zpow_le_zpow_left {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α} (hn : 0 ≤ n) (h : a ≤ b) : a ^ n ≤ b ^ n

theorem zsmul_le_zsmul_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 ≤ n) (h : a ≤ b) : n • a ≤ n • b

theorem zpow_lt_zpow_left {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) (h : a < b) : a ^ n < b ^ n

theorem zsmul_lt_zsmul_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) (h : a < b) : n • a < n • b

theorem zpow_le_zpow_iff_left {α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem zsmul_le_zsmul_iff_right {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) : n • a ≤ n • b ↔ a ≤ b

theorem zpow_lt_zpow_iff_left {α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) : a ^ n < b ^ n ↔ a < b

theorem zsmul_lt_zsmul_iff_right {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α} (hn : 0 < n) : n • a < n • b ↔ a < b

theorem not_isCyclic_of_denselyOrdered (α : Type u_1) [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α

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

theorem not_isAddCyclic_of_denselyOrdered (α : Type u_1) [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [DenselyOrdered α] [Nontrivial α] : ¬IsAddCyclic α

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