Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-15 00:15 c91fc150

View on Github →

chore(geometry/manifold/real_instances): use euclidean_space (#3077) Now that euclidean_space has been refactored to use the product topology, we can fix the geometry file that used a version of the product space (with the sup norm!) called euclidean_space2, using now instead the proper euclidean_space.

Estimated changes