mathlib

446eb51c - feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic as a module to the exterior algebra (#11468)

feat(linear_algebra/clifford_algebra): the clifford algebra is isomorphic as a module to the exterior algebra (#11468) The key result here is ```lean /-- 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.