mathlib3

10a586b1 - feat(linear_algebra): add module (vector_space) structure for function spaces