Commit 2021-01-04 22:10 78d5bd37

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.