Commit 2024-10-02 18:00 f01032b3
View on Github →chore: one_le_pow_of_one_le
-> one_le_pow₀
(#17215)
Rename:
pow_le_one
->pow_le_one₀
pow_lt_one
->pow_lt_one₀
one_le_pow_of_one_le
->one_le_pow₀
one_lt_pow
->one_lt_pow₀
and make all non-order arguments implicit (those are not rewrite lemmas, and where the explicit arguments are located is basically random throughout the library) From LeanAPAP