Anthony Bordg (Oct 11 2019 at 09:45): Anthony Bordg (Oct 11 2019 at 09:45):@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.
Anthony Bordg (Nov 28 2019 at 16:59):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: Jan 13 2026 at 20:28 UTC