mathlib3

ce50450d - chore(analysis/normed_space/linear_isometry): adjust `isometry` API (#9635)

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 definitions`linear_map.to_linear_isometry`, `linear_isometry_equiv.of_surjective`.