@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.
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