mathlib3

fe9c021d - feat(geometry/manifold/instances): sphere is a smooth manifold (#5607)

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. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>