# Commit 2021-01-04 22:10 78d5bd37

View on Github →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.