mathlib

2939c77d - feat(topology/metric_space): multiplicative opposites inherit the same `(pseudo_?)(e?)metric` and `uniform_space` (#12120)

feat(topology/metric_space): multiplicative opposites inherit the same `(pseudo_?)(e?)metric` and `uniform_space` (#12120) This puts the "obvious" metric on the opposite type such that `dist (op x) (op y) = dist x y`. This also merges `subtype.pseudo_dist_eq` and `subtype.dist_eq` as the latter was a special case of the former.