Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-19 23:24 cf118ee6

View on Github →

feat(analysis/complex/upper_half_plane): add upper_half_plane.mk (#14795)

Estimated changes

Modified src/analysis/complex/upper_half_plane/basic.lean

added theorem upper_half_plane.coe_mk

added def upper_half_plane.mk

added theorem upper_half_plane.mk_coe

added theorem upper_half_plane.mk_im

added theorem upper_half_plane.mk_re

added theorem upper_half_plane.re_add_im