Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes