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]>
leanprover-community · Aug 19, 2024 · 9b47769 · 9b47769
1 parent 48fd37e
commit 9b47769
Show file tree

Hide file tree

Showing 3 changed files with 419 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2884,6 +2884,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