feat(LinearAlgebra/CliffordAlgebra): port SpinGroup (#9111)

In this PR, we define `lipschitzGroup`, `pinGroup` and `spinGroup`, and prove some basic lemmas.

Ported from leanprover-community/mathlib3/pull/16040.

Co-authored-by: Jiale Miao <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>



Co-authored-by: utensil <[email protected]>
Co-authored-by: Utensil <[email protected]>

Author: eric-wieser

Mathlib.lean

@@ -2886,6 +2886,7 @@ import Mathlib.LinearAlgebra.CliffordAlgebra.Fold
 import Mathlib.LinearAlgebra.CliffordAlgebra.Grading
 import Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
 import Mathlib.LinearAlgebra.CliffordAlgebra.Prod
+import Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
 import Mathlib.LinearAlgebra.CliffordAlgebra.Star
 import Mathlib.LinearAlgebra.Coevaluation
 import Mathlib.LinearAlgebra.Contraction