mathlib

5f9e4277 - feat(analysis/normed_space/add_torsor): isometries of normed_add_torsors (#3666)

feat(analysis/normed_space/add_torsor): isometries of normed_add_torsors (#3666) Add the lemma that an isometry of `normed_add_torsor`s induces an isometry of the corresponding `normed_group`s at any base point. Previously discussed on Zulip, see <https://leanprover-community.github.io/archive/stream/113488-general/topic/Undergraduate.20math.20list.html#199450039>; both statement and proof have been revised along the lines indicated in that discussion.