Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-22 13:12 69071436

View on Github →

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.

Estimated changes