leanprover-community/mathlib4

Add typeclasses for smooth `(· • ·)`

Aperta

#5617 aperta il 30 giu 2023

Vedi su GitHubGuida contributor
 (1 commento) (0 reazioni) (0 assegnatari)Lean (1592 fork)github user discovery
good first issuet-differential-geometry

Metriche repository

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

Descrizione

  • 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.

Guida contributor

Direzione di ricerca
Aggiungi typeclass per la moltiplicazione liscia seguendo il modello di `ContinuousConstSMul` e `ContinuousSMul`. La prima typeclass deve essere per `∀ c, Smooth I I (c • ·)`, la seconda per `Smooth (I.prod J) J (Function.uncurry (· • ·))`.
Tech stack
Nessuno
Dominio
Nessuno
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Mezza giornata
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
LeanTypeclasses
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30