Commit 2021-01-13 10:19 b6cca97e

feat(linear_algebra/{exterior,tensor}_algebra): Prove that ι is injective (#5712) This strategy can't be used on clifford_algebra, and the obvious guess of trying to define a less_triv_sq_quadratic_form_ext leads to a non-associative multiplication; so for now, we just handle these two cases.