mathlib

ffb51d35 - feat(linear_algebra/clifford_algebra/basic): invertibility of vectors (#16077)

feat(linear_algebra/clifford_algebra/basic): invertibility of vectors (#16077) I believe the reverse direction of `is_unit_ι_of_is_unit` is true, but it requires that `Q` is divisible by two and #11468.