Commit 2023-12-18 07:15 d61c95e1
View on Github →chore: Rename pow monotonicity lemmas (#9095)
The names for lemmas about monotonicity of (a ^ ·)
and (· ^ n)
were a mess. This PR tidies up everything related by following the naming convention for (a * ·)
and (· * b)
. Namely, (a ^ ·)
is pow_right
and (· ^ n)
is pow_left
in lemma names. All lemma renames follow the corresponding multiplication lemma names closely.
Renames
Algebra.GroupPower.Order
pow_mono
→pow_right_mono
pow_le_pow
→pow_le_pow_right
pow_le_pow_of_le_left
→pow_le_pow_left
pow_lt_pow_of_lt_left
→pow_lt_pow_left
strictMonoOn_pow
→pow_left_strictMonoOn
pow_strictMono_right
→pow_right_strictMono
pow_lt_pow
→pow_lt_pow_right
pow_lt_pow_iff
→pow_lt_pow_iff_right
pow_le_pow_iff
→pow_le_pow_iff_right
self_lt_pow
→lt_self_pow
strictAnti_pow
→pow_right_strictAnti
pow_lt_pow_iff_of_lt_one
→pow_lt_pow_iff_right_of_lt_one
pow_lt_pow_of_lt_one
→pow_lt_pow_right_of_lt_one
lt_of_pow_lt_pow
→lt_of_pow_lt_pow_left
le_of_pow_le_pow
→le_of_pow_le_pow_left
pow_lt_pow₀
→pow_lt_pow_right₀
Algebra.GroupPower.CovariantClass
pow_le_pow_of_le_left'
→pow_le_pow_left'
nsmul_le_nsmul_of_le_right
→nsmul_le_nsmul_right
pow_lt_pow'
→pow_lt_pow_right'
nsmul_lt_nsmul
→nsmul_lt_nsmul_left
pow_strictMono_left
→pow_right_strictMono'
nsmul_strictMono_right
→nsmul_left_strictMono
StrictMono.pow_right'
→StrictMono.pow_const
StrictMono.nsmul_left
→StrictMono.const_nsmul
pow_strictMono_right'
→pow_left_strictMono
nsmul_strictMono_left
→nsmul_right_strictMono
Monotone.pow_right
→Monotone.pow_const
Monotone.nsmul_left
→Monotone.const_nsmul
lt_of_pow_lt_pow'
→lt_of_pow_lt_pow_left'
lt_of_nsmul_lt_nsmul
→lt_of_nsmul_lt_nsmul_right
pow_le_pow'
→pow_le_pow_right'
nsmul_le_nsmul
→nsmul_le_nsmul_left
pow_le_pow_of_le_one'
→pow_le_pow_right_of_le_one'
nsmul_le_nsmul_of_nonpos
→nsmul_le_nsmul_left_of_nonpos
le_of_pow_le_pow'
→le_of_pow_le_pow_left'
le_of_nsmul_le_nsmul'
→le_of_nsmul_le_nsmul_right'
pow_le_pow_iff'
→pow_le_pow_iff_right'
nsmul_le_nsmul_iff
→nsmul_le_nsmul_iff_left
pow_lt_pow_iff'
→pow_lt_pow_iff_right'
nsmul_lt_nsmul_iff
→nsmul_lt_nsmul_iff_left
Data.Nat.Pow
Nat.pow_lt_pow_of_lt_left
→Nat.pow_lt_pow_left
Nat.pow_le_iff_le_left
→Nat.pow_le_pow_iff_left
Nat.pow_lt_iff_lt_left
→Nat.pow_lt_pow_iff_left
Lemmas added
pow_le_pow_iff_left
pow_lt_pow_iff_left
pow_right_injective
pow_right_inj
Nat.pow_le_pow_left
to have the correct name sinceNat.pow_le_pow_of_le_left
is in Std.Nat.pow_le_pow_right
to have the correct name sinceNat.pow_le_pow_of_le_right
is in Std.
Lemmas removed
self_le_pow
was a duplicate ofle_self_pow
.Nat.pow_lt_pow_of_lt_right
is defeq topow_lt_pow_right
.Nat.pow_right_strictMono
is defeq topow_right_strictMono
.Nat.pow_le_iff_le_right
is defeq topow_le_pow_iff_right
.Nat.pow_lt_iff_lt_right
is defeq topow_lt_pow_iff_right
.
Other changes
- A bunch of proofs have been golfed.
- Some lemma assumptions have been turned from
0 < n
or1 ≤ n
ton ≠ 0
. - A few
Nat
lemmas have beenprotected
. - One docstring has been fixed.