The PR to Mathlib #9111 about Spin groups is ready to merge, but there are 2 open questions:
- what more lemmas about Spin groups are interesting to mathematians?
- what more should be formalized to formalize Versors and what’s in Section "The contents of a geometric algebra" in [chisolm2012geometric] , e.g. r-blades, r-vectors?
For the former, I should take a closer look at [figueroa2010spin] and maybe [suarez2019expository], [reynoso2023probing].
For the latter, see the Z-filteration in lean-ga and the prototype.
I also wish to include some latest results presented in [ruhe2023clifford], with supplements from [brehmer2023geometric] (lately there is a new paper applying this in HEP [spinner2024lorentz], in the same spirit, I should also read [berzins2024geometry] and possibly [raissi2019physics]), in which some of the results are proven in [roelfs2023graded].
See also discussions in the lean-ga blueprint.
I've started a Forester experiment about the definitions of Spin groups here. I also need to check citations of On some Lie groups in degenerate Clifford geometric algebras.