mathlib

78d5bd37 - feat(analysis/normed_space/{finite_dimension, inner_product}): assorted finite-dimensionality lemmas (#5580)

feat(analysis/normed_space/{finite_dimension, inner_product}): assorted finite-dimensionality lemmas (#5580) Two groups of lemmas about finite-dimensional normed spaces: - normed spaces of the same finite dimension are continuously linearly equivalent (this is a continuation of #5559) - variations on the existing lemma `submodule.findim_add_inf_findim_orthogonal`, that the dimensions of a subspace and its orthogonal complement sum to the dimension of the full space.