feat(geometry/manifold/instances/sphere): the differential of the embedding of the sphere into its ambient space (#16466)
feat(geometry/manifold/instances/sphere): the differential of the embedding of the sphere into its ambient space (#16466)


Formalized as part of the Sphere Eversion project.





leanprover-community/mathlib,leanprover-community/mathlib