Commit 2022-02-24 01:18 2939c77d

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.