leanprover-community/mathlib4

Rename `rpow_le_rpow`

Ouverte

#13 544 ouverte le 5 juin 2024

Voir sur GitHubGuide contributeur
 (4 commentaires) (0 réaction) (0 personne assignée)Lean (1 592 forks)github user discovery
good first issueplease-adopt

Métriques du dépôt

Stars
 (3 869 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

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.

Guide contributeur

Direction de recherche
Examinez les PRs de renommage précédentes (par exemple #9095, #9235, #18956) pour comprendre la convention de nommage, puis appliquez un renommage similaire à `rpow le rpow` et aux lemmes associés.
Stack technique
Aucun
Domaine
Aucun
Type d'issue
Refactorisation
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
2
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-3 heures
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Git
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
75