@Yijun He The sorry's left in Sphere2.thy are mere computations that could be easily flesh out, in particular they do not require any knowledge of differential geometry or Lie groups. So, it's probably the place to start.

sorry

Sphere2.thy

I cleaned the file today. Now, the theory compiles modulo the sorry's left. These sorry's only involve very straightforward algebraic manipulations.

Last updated: Dec 07 2023 at 16:21 UTC