Stream: Lie

Topic: Sphere2.thy


view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC