leanprover-community/mathlib4

Add typeclasses for smooth `(· • ·)`

Aberta

#5.617 aberto em 30 de jun. de 2023

Ver no GitHubGuia do colaborador
 (1 comentário) (0 reação) (0 responsável)Lean (1.592 forks)github user discovery
good first issuet-differential-geometry

Métricas do repositório

Stars
 (3.869 estrelas)
Métricas de merge de PR
 (Nenhuma PRs mesclada em 30d)

Description

  • Add a typeclass for ∀ c, Smooth I I (c • ·).
  • Add a typeclass for Smooth (I.prod J) J (Function.uncurry (· • ·))

See ContinuousConstSMul and ContinuousSMul for example of API.

Guia do colaborador

Direção de pesquisa
Adicione typeclasses para multiplicação suave seguindo o padrão de `ContinuousConstSMul` e `ContinuousSMul`. A primeira typeclass deve ser para `∀ c, Smooth I I (c • ·)`, e a segunda para `Smooth (I.prod J) J (Function.uncurry (· • ·))`.
Pilha de tecnologia
None
Domain
None
Tipo Issue
Funcionalidade
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
3
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
Meio dia
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
LeanTypeclasses
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
30