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

Estimated changes

deleted theorem one_le_pow_of_one_le
added theorem one_le_pow₀
deleted theorem one_lt_pow
added theorem one_lt_pow₀
deleted theorem pow_le_one
added theorem pow_le_one₀
deleted theorem pow_lt_one
added theorem pow_lt_one₀