3.2 Contents

This section would contain what’s in Section “The contents of a geometric algebra" in [ Chisolm(2012) ] , e.g. \(r\)-blades, \(r\)-vectors, before we can discuss anything about the GA operations.

That means we need to first formalize the counter parts in Clifford Algebra, e.g. Lipschitz Group, Spin Group, and Z-filteration in Clifford Algebra.

Jiale Miao’s mathlib#16040 (ported to Lean 4 as mathlib4#9111 ) seems to be a more principled attempt than versors in lean-ga except for the part involving Z-filteration which is still worth porting, possibly with ideas from the prototype here.

We also wish to include some latest results presented in [ Ruhe et al.(2023) ] , with supplements from [ Brehmer et al.(2023) ] , in which some of the results are proven in [ Roelfs and De Keninck(2023) ] .