leanprover-community/mathlib4

Add typeclasses for smooth `(· • ·)`

Offen

#5.617 geöffnet am 30.06.2023

Auf GitHub ansehenContributor Guide
 (1 Kommentar) (0 Reaktionen) (0 zugewiesene Personen)Lean (1.592 Forks)github user discovery
good first issuet-differential-geometry

Repository-Metriken

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

Beschreibung

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

Contributor Guide

Research-Richtung
Fügen Sie Typklassen für glatte Multiplikation nach dem Muster von `ContinuousConstSMul` und `ContinuousSMul` hinzu. Die erste Typklasse ist für `∀ c, Smooth I I (c • ·)`, die zweite für `Smooth (I.prod J) J (Function.uncurry (· • ·))`.
Tech Stack
Keine
Domain
Keine
Issue Type
Funktion
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
Halber Tag
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
LeanTypeclasses
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
30