Lemmas about the interaction of power operations with order #
See also smul_right_injective
. TODO: provide a NoZeroSMulDivisors
instance. We can't do
that here because importing that definition would create import cycles.
Alias of zsmul_right_inj
, for ease of discovery alongside zsmul_le_zsmul_iff'
and
zsmul_lt_zsmul_iff'
.
Alias of zpow_left_inj
, for ease of discovery alongside zsmul_le_zsmul_iff'
and
zsmul_lt_zsmul_iff'
.
See also pow_left_strictMono
and Nat.pow_left_strictMono
.
See also pow_right_strictMono'
.
Lemmas for canonically linear ordered semirings or linear ordered rings #
The slightly unusual typeclass assumptions [LinearOrderedSemiring R] [ExistsAddOfLE R]
cover two
more familiar settings:
[LinearOrderedRing R]
, egℤ
,ℚ
orℝ
[CanonicallyLinearOrderedSemiring R]
(although we don't actually have this typeclass), egℕ
,ℚ≥0
orℝ≥0
Alias of the reverse direction of Odd.pow_nonpos_iff
.
Alias of the reverse direction of Odd.pow_neg_iff
.
Alias of the reverse direction of sq_pos_iff
.
Alias of the reverse direction of sq_pos_iff
.
Alias of the reverse direction of sq_pos_iff
.
See also pow_left_strictMonoOn
.
Deprecated lemmas #
Those lemmas have been deprecated on 2023-12-23.
Alias of pow_right_mono
.
Alias of pow_le_pow_right
.
Alias of pow_le_pow_left
.
Alias of pow_lt_pow_left
.
Alias of pow_left_strictMonoOn
.
See also pow_left_strictMono
and Nat.pow_left_strictMono
.
Alias of pow_right_strictMono
.
See also pow_right_strictMono'
.
Alias of pow_lt_pow_right
.
Alias of pow_lt_pow_iff_right
.
Alias of pow_le_pow_iff_right
.
Alias of lt_self_pow
.
Alias of pow_right_strictAnti
.
Alias of pow_lt_pow_iff_right_of_lt_one
.
Alias of pow_lt_pow_right_of_lt_one
.
Alias of lt_of_pow_lt_pow_left
.
Alias of le_of_pow_le_pow_left
.
Alias of le_self_pow
.
Alias of pow_lt_pow_right
.
Alias of pow_right_strictMono
.
See also pow_right_strictMono'
.
Alias of pow_le_pow_iff_right
.
Alias of pow_lt_pow_iff_right
.