leanprover-community/mathlib4

Rename `rpow_le_rpow`

Aperta

#13.544 aperta il 5 giu 2024

Vedi su GitHubGuida contributor
 (4 commenti) (0 reazioni) (0 assegnatari)Lean (1592 fork)github user discovery
good first issueplease-adopt

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

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.

Guida contributor

Direzione di ricerca
Esamina le PR di ridenominazione precedenti (es. #9095, #9235, #18956) per comprendere la convenzione di denominazione, quindi applica una ridenominazione simile a `rpow le rpow` e ai lemmi correlati.
Tech stack
Nessuno
Dominio
Nessuno
Tipo issue
Refactoring
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
2
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Git
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
75