leanprover-community/mathlib4

Add typeclasses for smooth `(· • ·)`

オープン

#5,617 opened on 2023/06/30

 (1 件のコメント) (0 件のリアクション) (0 人の担当者)Lean (1,592 件のフォーク)github user discovery
good first issuet-differential-geometry

Repository metrics

Stars
 (3,869 個のスター)
PR merge metrics
 (30d に merged PR はありません)

説明

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

コントリビューターガイド