mathlib3

b6cca97e - feat(linear_algebra/{exterior,tensor}_algebra): Prove that `ι` is injective (#5712)

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. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>