Mathlib v3 is deprecated. Go to Mathlib v4

Structure euclidean_geometry.sphere

Modification history

2023-03-18 09:58
src/geometry/euclidean/sphere/basic.lean
chore(geometry/euclidean/sphere/basic): generalize typeclasses (#18605) …
Modified euclidean_geometry.sphereView on Github →
2023-03-16 11:15
src/geometry/euclidean/basic.lean
refactor(geometry/euclidean): split out spheres (#18220) …
Modified euclidean_geometry.sphereView on Github →
2022-10-05 09:32
src/geometry/euclidean/basic.lean
feat(geometry/euclidean/basic): bundled spheres (#16184) …
Added euclidean_geometry.sphereView on Github →