mathlib3
2e562102 - chore(analysis/complex/upper_half_plane): don't use `abbreviation` (#12679)

Commit
3 years ago
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`.
Author
Parents
Loading