mathlib

007d6602 - feat(analysis/inner_product_space/pi_L2): `map_isometry_euclidean_of_orthonormal` (#11907)

feat(analysis/inner_product_space/pi_L2): `map_isometry_euclidean_of_orthonormal` (#11907) Add a lemma giving the result of `isometry_euclidean_of_orthonormal` when applied to an orthonormal basis obtained from another orthonormal basis with `basis.map`.