Documentation

LeanPool.LeanModularForms.Modularforms.Upperhalfplane

Upperhalfplane #

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