leanprover-community/mathlib4

Add typeclasses for smooth `(· • ·)`

Ouverte

#5 617 ouverte le 30 juin 2023

Voir sur GitHubGuide contributeur
 (1 commentaire) (0 réaction) (0 personne assignée)Lean (1 592 forks)github user discovery
good first issuet-differential-geometry

Métriques du dépôt

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

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.

Guide contributeur

Direction de recherche
Ajoutez des classes de types pour la multiplication lisse en suivant le modèle de `ContinuousConstSMul` et `ContinuousSMul`. La première classe de types doit être pour `∀ c, Smooth I I (c • ·)`, et la seconde pour `Smooth (I.prod J) J (Function.uncurry (· • ·))`.
Stack technique
Aucun
Domaine
Aucun
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Une demi journée
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
LeanTypeclasses
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
30