Commit 2020-08-03 17:57 5f9e4277

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