mathlib

027ff1e4 - chore(geometry/euclidean/sphere/basic): generalize typeclasses (#18605)

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`