Commit 2023-03-18 09:58 027ff1e4

chore(geometry/euclidean/sphere/basic): generalize typeclasses (#18605) cospherical_empty asks for P to be a real inner product space when all it needs is nonempty P. The motivation for this PR is that it fixes a linter error in #18583; lean complains that we are carrying around the type V for no reason. The alternative here would be to force all these typeclass arguments to be present in the constructor for euclidean_space.sphere and use no_lint unused_arguments