mathlib

8fa3263c - fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450)

fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450) I'm doing this because I need to have `balanced_hull_core` before `normed_space.finite_dimensional` and this little change seems to be enough for that, but I think at some point we'll need to move lemmas so that normed_spaces come as late as possible