isometry): move material about isometries of normed spaces (#8003)

Commit

4 years ago

refactor(topology/metric_space/isometry): move material about isometries of normed spaces (#8003) See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/topology.20and.20analysis

Author

hrmacbeth

Parents

7d5b50a7

mathlib 7d155d95 - refactor(topology/metric_space/isometry): move material about isometries of normed spaces (#8003)

mathlib
7d155d95 - refactor(topology/metric_space/isometry): move material about isometries of normed spaces (#8003)