Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 18:29 fe9c021d

View on Github →

feat(geometry/manifold/instances): sphere is a smooth manifold (#5607) Put a smooth manifold structure on the sphere, and provide tools for constructing smooth maps to and from the sphere.

Estimated changes