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
.