feat(linear_algebra/clifford_algebra/spin_group) : Spin Group

[Biiiilly]

In this file we define lipschitz , pin_group and spin_group.

Here are some discussion about the latent ambiguity of definition :
https://mathoverflow.net/q/427881/172242 and https://mathoverflow.net/q/251288/172242

The definition of the Lipschitz group {𝑥 ∈ 𝐶𝑙(𝑉,𝑞) │ 𝑥 𝑖𝑠 𝑖𝑛𝑣𝑒𝑟𝑡𝑖𝑏𝑙𝑒 𝑎𝑛𝑑 𝑥𝑣𝑥⁻¹∈ 𝑉} is given by:
• Fulton, W. and Harris, J., 2004. Representation theory. New York: Springer, p.chapter 20.
• https://en.wikipedia.org/wiki/Clifford_algebra#Lipschitz_group
But they presumably form a group only in finite dimensions. So we define lipschitz with closure of
all the elements in the form of ι Q m. We show this definition is at least as large as the
other definition (See mem_lipschitz_conj_act_le and mem_lipschitz_involute_le) and the reverse
statement presumably being true only in finite dimensions.

Note that the proofs of mem_lipschitz_conj_act_le and mem_lipschitz_involute_le are blocked by some PRs shown below.

---

• depends on: [Merged by Bors] - feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic as a module to the exterior algebra #11468 [clifford algebra is isomorphic to exterior algebra if invertible 2]
• depends on: [Merged by Bors] - feat(algebra/invertible): map_inv_of and some other basic results #16202 [f (⅟r) = ⅟(f r)]
• depends on: [Merged by Bors] - feat(linear_algebra/clifford_algebra/basic): lemmas about triple products of repeated vectors #16153 [triple products of repeated vectors]

[Biiiilly]

Note that the proofs of mem_lipschitz_conj_act_le and mem_lipschitz_involute_le are blocked by some PRs.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic as a module to the exterior algebra #11468
• [Merged by Bors] - feat(algebra/invertible): map_inv_of and some other basic results #16202
• [Merged by Bors] - feat(linear_algebra/clifford_algebra/basic): lemmas about triple products of repeated vectors #16153
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

Any more ideas on how to prove this or under what situations it's true?

[Biiiilly]

I already got the proof of this. I just need some time to tidy it up.

[eric-wieser]

Could you commit the messy version somewhere so that it doesn't get lost?

[utensil]

Could you commit the messy version somewhere so that it doesn't get lost?

@Biiiilly Hi, I'm trying to make this PR work in Lean 4, do you still have the proof of this?