Commit 2022-06-20 11:25 c1abe061

refactor(linear_algebra/exterior_algebra): redefine exterior_algebra as clifford_algebra 0 (#14819) The motivation here is to avoid having to duplicate API between these two types, else we end up having to repeat every definition that works on clifford_algebra Q on exterior_algebra for the case when Q = 0. This also:

• Removes as_exterior : clifford_algebra (0 : quadratic_form R M) ≃ₐ[R] exterior_algebra R M as the two types are reducibly defeq.
• Removes support for working with exterior algebras over semirings; while it is entirely possible to generalize clifford_algebra to semirings to make this removal unnecessary, it creates difficulties with elaboration, and the support for semirings was without mathematical motivation in the first place. This is in line with a vote on Zulip. The consequences are:
• A bunch of redundant code can be removed
• x.reverse and x.involute should now work on x : exterior_algebra R M.
• Future API will extend effortlessly from one to the other