English
For h ≠ 0, for each z ∈ ℂ there exists m ∈ ℤ such that invQParam(h, qParam(h,z)) = z + m·h.
Русский
Для любого z ∈ ℂ существует m ∈ ℤ такое, что invQParam(h, qParam(h,z)) = z + m·h.
LaTeX
$$$\forall h \; h \neq 0 \; \forall z \in \mathbb{C},\; \exists m \in \mathbb{Z},\; \mathrm{invQParam}(h, \mathrm{qParam}(h,z)) = z + m \cdot h$$$
Lean4
theorem qParam_left_inv_mod_period (hh : h ≠ 0) (z : ℂ) : ∃ m : ℤ, invQParam h (𝕢 h z) = z + m * h :=
by
dsimp only [qParam, invQParam]
obtain ⟨m, hm⟩ := log_exp_exists (2 * ↑π * I * z / ↑h)
refine
⟨m, by
rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc, div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add,
mul_div_cancel₀ _ (mod_cast hh), mul_comm]⟩