mathlib3

432e85ef - feat(analysis/normed_space/linear_isometry): add congr_arg and congr_fun (#11428)

feat(analysis/normed_space/linear_isometry): add congr_arg and congr_fun (#11428) Two trivial lemmas that are missing from this bundled morphism but present on most others. Turns out I didn't actually need these in the branch I created them in, but we should have them anyway.