issue !4#13544: Rename `zpow_le_zpow` and `rpow_le_rpow`

Stream: triage

[Random Issue Bot]

Today I chose issue 13544 for discussion!

Rename zpow_le_zpow and rpow_le_rpow
Created by @Bolton Bailey (@BoltonBailey) on 2024-06-05
Labels: good first issue, please-adopt

Is this issue still relevant? Any recent updates? Anyone making progress?

[Bolton Bailey]

I am treating this issue as a potential good first issue for newcomers who want to try their hand at a mathlib PR. Is there some way to avoid the triage bot posting issues like this?