Theorem contMDiff_circleExp

Modification history

2024-11-25 11:42

Mathlib/Geometry/Manifold/Instances/Sphere.lean

feat: extend `ContDiff` to take a smoothness exponent in `WithTop ℕ∞` (#19442) …

Modified contMDiff_circleExp View on Github →

2024-08-13 09:26

Mathlib/Geometry/Manifold/Instances/Sphere.lean

refactor: Make `circle` a type `Circle` (#15116) …

Added contMDiff_circleExp View on Github →