leanprover-community/mathlib4

Rename `rpow_le_rpow`

Offen

#13.544 geöffnet am 05.06.2024

Auf GitHub ansehenContributor Guide
 (4 Kommentare) (0 Reaktionen) (0 zugewiesene Personen)Lean (1.592 Forks)github user discovery
good first issueplease-adopt

Repository-Metriken

Stars
 (3.869 Sterne)
PR-Merge-Metriken
 (Keine gemergten PRs in 30 T)

Beschreibung

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-Richtung
Überprüfe die vorherigen Umbenennungs PRs (z. B. #9095, #9235, #18956), um die Namenskonvention zu verstehen, und wende dann eine ähnliche Umbenennung auf `rpow le rpow` und die zugehörigen Lemmata an.
Tech Stack
Keine
Domain
Keine
Issue Type
Refactoring
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
2
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-3 Stunden
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
Git
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
75