mathlib3

f44e6697 - chore(linear_algebra/exterior_algebra): Avoid the unhelpful exterior_algebra.quot definition