Documentation

Mathlib.Algebra.Order.Group.Basic

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

instance instIsMulTorsionFree {α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] :

IsMulTorsionFree α

instance instIsAddTorsionFree {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] :

IsAddTorsionFree α

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

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.