Documentation
SpherePacking
.
ModularForms
.
upperhalfplane
Search
return to top
source
Imports
Init
Mathlib.Data.Real.StarOrdered
Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Imported by
pnat_div_upper
pos_nat_div_upper
source
theorem
pnat_div_upper
(
n
:
ℕ+
)
(
z
:
UpperHalfPlane
)
:
0
<
(
-
↑
↑
n
/
↑
z
).
im
source
theorem
pos_nat_div_upper
(
n
:
ℤ
)
(
hn
:
0
<
n
)
(
z
:
UpperHalfPlane
)
:
0
<
(
-
↑
n
/
↑
z
).
im