Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 17:36 2e562102

View on Github →

chore(analysis/complex/upper_half_plane): don't use abbreviation (#12679) Some day we should add Poincaré metric as a metric_space instance on upper_half_plane. In the meantime, make sure that Lean doesn't use subtype instances for uniform_space and/or metric_space.

Estimated changes