mathlib3
b834415b - chore(topology/metric_space/gromov_hausdorff): Golf some theorems (#11591)

Commit

3 years ago

chore(topology/metric_space/gromov_hausdorff): Golf some theorems (#11591)

Author

vihdzp

vihdzp

Parents

Loading