leanprover-community/mathlib4

Add typeclasses for smooth `(· • ·)`

Open

#5,617 opened on Jun 30, 2023

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Lean (1,381 forks)github user discovery
good first issuet-differential-geometry

Repository metrics

Stars
 (3,405 stars)
PR merge metrics
 (No merged PRs in 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.

Contributor guide

Research direction
Add typeclasses for smooth multiplication following the pattern of `ContinuousConstSMul` and `ContinuousSMul`. The first typeclass should be for `∀ c, Smooth I I (c • ·)`, and the second for `Smooth (I.prod J) J (Function.uncurry (· • ·))`.
Tech stack
None
Domain
None
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
Half day
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
LeanTypeclasses
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30