Basic lemmas about ordered rings #
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
.
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
.