mathlib3
refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible
#1052
Merged
Merged