Lemmas about the interaction of power operations with order #
theorem
one_lt_zpow'
{α : Type u_1}
[OrderedCommGroup α]
{n : ℤ}
{a : α}
(ha : 1 < a)
(hn : 0 < 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_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_le_zsmul'
{α : Type u_1}
[OrderedAddCommGroup α]
{n : ℤ}
{a : α}
{b : α}
(hn : 0 ≤ n)
(h : a ≤ b)
:
theorem
zpow_le_zpow'
{α : Type u_1}
[OrderedCommGroup α]
{n : ℤ}
{a : α}
{b : α}
(hn : 0 ≤ n)
(h : a ≤ b)
:
theorem
zsmul_lt_zsmul'
{α : Type u_1}
[OrderedAddCommGroup α]
{n : ℤ}
{a : α}
{b : α}
(hn : 0 < n)
(h : a < b)
:
theorem
zpow_lt_zpow'
{α : Type u_1}
[OrderedCommGroup α]
{n : ℤ}
{a : α}
{b : α}
(hn : 0 < n)
(h : 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_eq_zsmul_iff'
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{n : ℤ}
{a : α}
{b : α}
(hn : n ≠ 0)
:
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)
:
Alias of zpow_left_inj, for ease of discovery alongside zsmul_le_zsmul_iff' and
zsmul_lt_zsmul_iff'.