Rename `zpow_le_zpow` and `rpow_le_rpow`

leanprover-community / mathlib4

The math library of Lean 4

https://leanprover-community.github.io/mathlib4_docs

Apache License 2.0

1.51k stars 332 forks source link

Rename `zpow_le_zpow` and `rpow_le_rpow` #13544

Open BoltonBailey opened 4 months ago

BoltonBailey commented 4 months ago

Pull requests #9095 and #9235 renamed pow_le_pow and a host of related lemmas to have more unambiguous names. It would be nice if analogous renaming could be done for zpow_le_zpow and rpow_le_rpow and company.

arulandu commented 1 month ago

@BoltonBailey Would love to work on this!