mathlib

02c9d69d - feat(analysis/inner_product_space/basic): `orthonormal.map_linear_isometry_equiv` (#11893)

feat(analysis/inner_product_space/basic): `orthonormal.map_linear_isometry_equiv` (#11893) Add a variant of `orthonormal.comp_linear_isometry_equiv` for the case of an orthonormal basis mapped with `basis.map`. If in future we get a bundled type of orthonormal bases with its own `map` operation, this would no longer be a separate lemma, but until then it's useful.