mathlib3

e29dfc19 - chore(analysis/normed_space/finite_dimensional): restructure imports (#9289)

chore(analysis/normed_space/finite_dimensional): restructure imports (#9289) Delays importing `linear_algebra.finite_dimensional` in the `analysis/normed_space/` directory until it is really needed. This reduces the ["long pole"](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib) of mathlib compilation by 3 minutes (out of 55). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>