feat(analysis/normed_space): define linear isometries (#5867)
* define `linear_isometry` and `linear_isometry_equiv`;
* add `linear_map.ker_eq_bot_of_inverse`;
* replace `inv_fun_apply` lemmas with `inv_fun_eq_symm`;
* golf some proofs in `linear_algebra/finite_dimensional`.
