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
one_lt_zpow
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a : α}
(ha : 1 < a)
(hn : 0 < n)
:
theorem
zsmul_pos
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{n : ℤ}
{a : α}
(ha : 0 < a)
(hn : 0 < n)
:
@[deprecated one_lt_zpow (since := "2024-11-13")]
theorem
one_lt_zpow'
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a : α}
(ha : 1 < a)
(hn : 0 < n)
:
Alias of one_lt_zpow
.
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 : ℤ}
:
theorem
zsmul_left_inj
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{a : α}
(ha : 0 < a)
{m n : ℤ}
:
theorem
zpow_right_mono
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{a : α}
(ha : 1 ≤ a)
:
theorem
zsmul_left_mono
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{a : α}
(ha : 0 ≤ a)
:
@[deprecated zpow_right_mono (since := "2024-11-13")]
theorem
zpow_mono_right
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{a : α}
(ha : 1 ≤ a)
:
Alias of zpow_right_mono
.
theorem
zpow_le_zpow_right
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 ≤ a)
(h : m ≤ n)
:
theorem
zsmul_le_zsmul_left
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{m n : ℤ}
{a : α}
(ha : 0 ≤ a)
(h : m ≤ n)
:
@[deprecated zpow_le_zpow_right (since := "2024-11-13")]
theorem
zpow_le_zpow
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 ≤ a)
(h : m ≤ n)
:
Alias of zpow_le_zpow_right
.
theorem
zpow_lt_zpow_right
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 < a)
(h : m < n)
:
theorem
zsmul_lt_zsmul_left
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{m n : ℤ}
{a : α}
(ha : 0 < a)
(h : m < n)
:
@[deprecated zpow_lt_zpow_right (since := "2024-11-13")]
theorem
zpow_lt_zpow
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 < a)
(h : m < n)
:
Alias of zpow_lt_zpow_right
.
theorem
zpow_le_zpow_iff_right
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 < a)
:
theorem
zsmul_le_zsmul_iff_left
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{m n : ℤ}
{a : α}
(ha : 0 < a)
:
@[deprecated zpow_le_zpow_iff_right (since := "2024-11-13")]
theorem
zpow_le_zpow_iff
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 < a)
:
Alias of zpow_le_zpow_iff_right
.
theorem
zpow_lt_zpow_iff_right
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 < a)
:
theorem
zsmul_lt_zsmul_iff_left
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{m n : ℤ}
{a : α}
(ha : 0 < a)
:
@[deprecated zpow_lt_zpow_iff_right (since := "2024-11-13")]
theorem
zpow_lt_zpow_iff
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{m n : ℤ}
{a : α}
(ha : 1 < a)
:
Alias of zpow_lt_zpow_iff_right
.
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
@[deprecated zpow_left_strictMono (since := "2024-11-13")]
theorem
zpow_strictMono_left
(α : Type u_1)
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
(hn : 0 < n)
:
StrictMono fun (x : α) => x ^ n
Alias of zpow_left_strictMono
.
theorem
zpow_left_mono
(α : Type u_1)
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
(hn : 0 ≤ n)
:
theorem
zsmul_mono_right
(α : Type u_1)
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{n : ℤ}
(hn : 0 ≤ n)
:
@[deprecated zpow_left_mono (since := "2024-11-13")]
theorem
zpow_mono_left
(α : Type u_1)
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
(hn : 0 ≤ n)
:
Alias of zpow_left_mono
.
theorem
zpow_le_zpow_left
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 ≤ n)
(h : a ≤ b)
:
theorem
zsmul_le_zsmul_right
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 ≤ n)
(h : a ≤ b)
:
@[deprecated zpow_le_zpow_left (since := "2024-11-13")]
theorem
zpow_le_zpow'
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 ≤ n)
(h : a ≤ b)
:
Alias of zpow_le_zpow_left
.
theorem
zpow_lt_zpow_left
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
(h : a < b)
:
theorem
zsmul_lt_zsmul_right
{α : Type u_1}
[AddCommGroup α]
[PartialOrder α]
[IsOrderedAddMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
(h : a < b)
:
@[deprecated zpow_lt_zpow_left (since := "2024-11-13")]
theorem
zpow_lt_zpow'
{α : Type u_1}
[CommGroup α]
[PartialOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
(h : a < b)
:
Alias of zpow_lt_zpow_left
.
theorem
zpow_le_zpow_iff_left
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
:
theorem
zsmul_le_zsmul_iff_right
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
:
@[deprecated zpow_le_zpow_iff_left (since := "2024-11-13")]
theorem
zpow_le_zpow_iff'
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
:
Alias of zpow_le_zpow_iff_left
.
theorem
zpow_lt_zpow_iff_left
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
:
theorem
zsmul_lt_zsmul_iff_right
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
:
@[deprecated zpow_lt_zpow_iff_left (since := "2024-11-13")]
theorem
zpow_lt_zpow_iff'
{α : Type u_1}
[CommGroup α]
[LinearOrder α]
[IsOrderedMonoid α]
{n : ℤ}
{a b : α}
(hn : 0 < n)
:
Alias of zpow_lt_zpow_iff_left
.
instance
instIsAddTorsionFree
{α : Type u_1}
[AddCommGroup α]
[LinearOrder α]
[IsOrderedAddMonoid α]
:
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 α]
:
A nontrivial densely linear ordered additive commutative group can't be a cyclic group.