Commit 2022-10-08 20:02 446eb51c

feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic as a module to the exterior algebra (#11468) The key result here is

/-- The module isomorphism to the exterior algebra -/
def equiv_exterior [invertible (2 : R)] : clifford_algebra Q ≃ₗ[R] exterior_algebra R M :=

There are a handful of intermediate definitions that are needed to get here that are missing lots of useful (but difficult) API lemmas, but I don't expect to have time to address those for a while. Probably the main missing result is that equiv_exterior preserves reversion.