feat(LinearAlgebra/CliffordAlgebra): port SpinGroup

[utensil]

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

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

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

---

This PR is a port of leanprover-community/mathlib#16040 .

• [x] Port all contents of leanprover-community/mathlib#16040
• [x] Prove invertible_of_invertible_ι missing from leanprover-community/mathlib#16040 (with @eric-wieser 's help)
  • [x] depends on: #9076
• [x] Pass CI
• [x] Write a proper commit message for the PR, adding all co-authors and deps
• [x] Fix naming issues
• [x] Fix style issues
• [x] Remove macro_rules
• [x] Minimize imports and deps
• [x] Add porting notes as PR comments
• [x] Rename lipschitz to lipschitzGroup and update doc, commit log etc.
• [x] Mark regressions from Lean 3 in this PR

This PR can be reviewed here or discussed on Zulip.