Commit 2022-02-10 20:43 007d6602
View on Github →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.