mathlib

1a72f887 - feat(analysis/inner_product_space/basic): isometries and orthonormal families (#11631)

feat(analysis/inner_product_space/basic): isometries and orthonormal families (#11631) Add various lemmas and definitions about the action of isometries on orthonormal families of vectors. An isometry preserves the property of being orthonormal; a linear map sending an orthonormal basis to an orthonormal family is a linear isometry, and a linear equiv sending an orthonormal basis to an orthonormal family is a linear isometry equiv. A definition `orthonormal.equiv` is provided that uses `basis.equiv` to provide a linear isometry equiv mapping a given orthonormal basis to another given orthonormal basis, and lemmas are provided analogous to those for `basis.equiv` (`orthonormal.map_equiv` isn't a `simp` lemma because `simp` can prove it).