Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-19 23:38 7d155d95

View on Github →

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

Estimated changes

Modified src/analysis/normed_space/add_torsor.lean

Modified src/analysis/normed_space/basic.lean

added theorem add_monoid_hom.isometry_iff_norm

added theorem add_monoid_hom.isometry_of_norm

added theorem algebra_map_isometry

added theorem isometric.add_left_symm

added theorem isometric.add_left_to_equiv

added theorem isometric.add_right_apply

added theorem isometric.add_right_symm

added theorem isometric.add_right_to_equiv

added theorem isometric.coe_add_left

added theorem isometric.coe_add_right

added theorem isometric.coe_neg

added theorem isometric.neg_symm

added theorem isometric.neg_to_equiv

added theorem uniform_space.completion.norm_coe

Modified src/analysis/normed_space/linear_isometry.lean

Modified src/analysis/normed_space/normed_group_hom.lean

Modified src/topology/algebra/group_completion.lean

Deleted src/topology/algebra/normed_group.lean

deleted theorem uniform_space.completion.norm_coe

Modified src/topology/metric_space/completion.lean

Modified src/topology/metric_space/isometry.lean

deleted theorem add_monoid_hom.isometry_iff_norm

deleted theorem add_monoid_hom.isometry_of_norm

deleted theorem algebra_map_isometry

deleted theorem isometric.add_left_symm

deleted theorem isometric.add_left_to_equiv

deleted theorem isometric.add_right_apply

deleted theorem isometric.add_right_symm

deleted theorem isometric.add_right_to_equiv

deleted theorem isometric.coe_add_left

deleted theorem isometric.coe_add_right

deleted theorem isometric.coe_neg

deleted theorem isometric.neg_symm

deleted theorem isometric.neg_to_equiv