mathlib3

c1abe061 - refactor(linear_algebra/exterior_algebra): redefine `exterior_algebra` as `clifford_algebra 0` (#14819)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exterior.20algebras.20over.20semiring/near/286660821). 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