mathlib3

3e77fec2 - feat(linear_algebra/finite_dimensional): finite dimensional vector spaces (#1241)

feat(linear_algebra/finite_dimensional): finite dimensional vector spaces (#1241) * feat(linear_algebra/finite_dimensional): finite dimensional vector spaces * rw `of_span_finite_eq_top` to `of_fg` * prove infinite.nat_embedding * generalize finite_of_linear_independent to noetherian modules * fix build * fix build (ring_theory/polynomial)