feat(linear_algebra/clifford): make clifford_algebra irreducible in a Lean4 compatible way

[sgouezel]

clifford_algebra is a complicated object (building on tensor_algebra which builds on free_algebra), which means Lean has difficulties working with it unless it is irreducible. In the current version, it is marked as irreducible after the fact, which is not Lean4-compatible. Instead, we switch to a construction as a one-field structure, which is genuinally irreducible (modelled on what is done for real numbers).

Part of #18164

---

[eric-wieser]

We're currently hundreds of dependencies away from being able to port this file. I'd be curious to see whether we run into trouble with the reducible definition in Lean 4, before committing to all the boilerplate this entails; so would be tempted to leave this PR sitting around for a while until we get closer.

[sgouezel]

We can definitely keep this around and only use it if necessary. Note however that in Lean 3, unmarking clifford_algebra as irreducible breaks a lot -- which is not surprising to me, since the construction is a three-fold scaffolding around free_algebra, so whenever Lean thinks it's a good idea to unfold the definition of multiplication, say, to see if it's defeq to something, then you're doomed to failure because things get exponentially big. I have the impression that making things genuinely irreducible can only help here, by adding an abstraction barrier even for the kernel (after all, we don't care at all about the inner workings of the definition, we only want its universal property).

[jcommelin]

Thanks 🎉

bors merge

[eric-wieser]

@jcommelin, I'd prefer to leave this PR open until this file gets closer to being portable

bors r-

bors d+

[bors]

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Canceled.

[eric-wieser]

We're now on the cusp of being able to port this; I've left a note on the port comment page remarking that if we run intro trouble while porting, these changes might be useful.