leanprover-community/mathlib4

Rename `rpow_le_rpow`

Aberta

#13.544 aberto em 5 de jun. de 2024

Ver no GitHubGuia do colaborador
 (4 comentários) (0 reação) (0 responsável)Lean (1.592 forks)github user discovery
good first issueplease-adopt

Métricas do repositório

Stars
 (3.869 estrelas)
Métricas de merge de PR
 (Nenhuma PRs mesclada em 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.

Guia do colaborador

Direção de pesquisa
Revise as PRs de renomeação anteriores (por exemplo, #9095, #9235, #18956) para entender a convenção de nomenclatura e aplique uma renomeação semelhante a `rpow le rpow` e seus lemas relacionados.
Pilha de tecnologia
None
Domain
None
Tipo Issue
Refatoração
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
2
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
1-3 horas
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Ativo
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Claro
Prerequisites
Git
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
75