mathlib

c720ca16 - chore(number_theory/modular_forms): don't define jacobi_theta on subtype (#19029)

chore(number_theory/modular_forms): don't define jacobi_theta on subtype (#19029) In a previous PR, the Jacobi theta function was defined on the subtype `ℍ` of `ℂ` and this is slightly annoying to work with. This PR tweaks it to be a function on `ℂ` (whose values outside `ℍ` are uninteresting, but well-defined). Split off from #19027.