Commit 2021-10-09 07:26 ce50450d

chore(analysis/normed_space/linear_isometry): adjust isometry API (#9635) Now that we have the linear_isometry definition, it is better to pass through this definition rather then using a linear_map satisfying the isometry hypothesis. To this end, convert old lemma linear_map.norm_apply_of_isometry to a new definition linear_map.to_linear_isometry, and delete old definition continuous_linear_equiv.of_isometry, whose use should be replaced by the pair of definitionslinear_map.to_linear_isometry, linear_isometry_equiv.of_surjective.