mathlib3

c8f30551 - feat(topology/metric_space): diameter of pointwise zero and addition (#19028)