mathlib3
feat(linear_algebra/finite_dimensional): finite dimensional vector spaces
#1241
Merged
Merged