Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-01 22:13 d08d5095

View on Github →

fix(metric_space/gromo_hausdorff): lemma should be instance + linting (#1840)

Estimated changes