mathlib3

6ed8b4b0 - feat(linear_algebra/finite_dimensional): lemmas for zero dimensional vector spaces (#6397)