Spherical coordinates

Stream: Is there code for X?

[ZhiKai Pong]

Hi, I'm looking to implement spherical coordinates in PhysLean, and I'd just like to check that mathlib currently doesn't have them either? I only found docs#polarCoord

[Joseph Tooby-Smith]

Following a discussion on the PhysLean channel (and more for the 'record' here rather than else), there is docs#homeomorphUnitSphereProd which splits a point up into a radius and a point on the sphere. Not quite fully into spherical coordinates though.