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.