leanprover-community/mathlib4

Rename `rpow_le_rpow`

Open

#13,544 opened on Jun 5, 2024

View on GitHub
 (4 comments) (0 reactions) (0 assignees)Lean (1,381 forks)github user discovery
good first issueplease-adopt

Repository metrics

Stars
 (3,405 stars)
PR merge metrics
 (No merged PRs in 30d)

Description

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

Contributor guide

Research direction
Review the previous renaming PRs (e.g., #9095, #9235, #18956) to understand the naming convention, then apply similar renaming to `rpow le rpow` and its related lemmas.
Tech stack
None
Domain
None
Issue type
Refactor
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
2
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-3 hours
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
Git
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
75