mathlib3

feat(topology/metric_space/isometry): add_left/right, neg

#2234

Merged