Commit 2021-01-29 17:21 aabb8436

View on Github →

feat(analysis/normed_space/inner_product): existence of isometry to Euclidean space (#5949) A finite-dimensional inner product space admits an isometry (expressed using the new linear_isometry_equiv structure of #5867, cc @urkud) to Euclidean space.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added theorem exists_is_orthonormal_basis'

added theorem is_R_or_C.inner_apply

deleted def is_basis.equiv_fun_euclidean

added def is_basis.isometry_euclidean_of_orthonormal

added def linear_isometry_equiv.of_inner_product_space

added theorem orthonormal.comp

added theorem orthonormal.inner_left_fintype

added theorem orthonormal.inner_right_fintype

added theorem pi_Lp.inner_apply

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.equiv_fin_of_dim_eq