qParam_right_inv — Mathlib

English

If h ≠ 0 and q ≠ 0, then qParam(h, invQParam(h,q)) = q.

Русский

Если h ≠ 0 и q ≠ 0, то qParam(h, invQParam(h,q)) = q.

LaTeX

$$$ h \neq 0 \Rightarrow q \neq 0 \Rightarrow \mathrm{qParam}(h, \mathrm{invQParam}(h,q)) = q$$$

Lean4

theorem qParam_right_inv (hh : h ≠ 0) {q : ℂ} (hq : q ≠ 0) : 𝕢 h (invQParam h q) = q := by
  simp only [qParam, invQParam, ← mul_assoc, mul_div_cancel₀ _ two_pi_I_ne_zero,
    mul_div_cancel_left₀ _ (ofReal_ne_zero.mpr hh), exp_log hq]

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