qParam_left_inv_mod_period — Mathlib

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]⟩

Похожие утверждения