one_sub_eta_q_ne_zero — Mathlib

English

For n ∈ ℕ and z in the upper half-plane, 1 − η_q(n,z) ≠ 0.

Русский

Для n ∈ ℕ и z в верхней полуплоскости, 1 − η_q(n,z) ≠ 0.

LaTeX

$$$1 - \\eta_q(n,z) \\neq 0$$$

Lean4

theorem one_sub_eta_q_ne_zero (n : ℕ) {z : ℂ} (hz : z ∈ ℍₒ) : 1 - eta_q n z ≠ 0 :=
  by
  rw [eta_q_eq_cexp, sub_ne_zero]
  intro h
  simpa [← mul_assoc, ← h] using
    norm_exp_two_pi_I_lt_one ⟨(n + 1) • z, by simpa [(show 0 < (n + 1 : ℝ) by positivity)] using hz⟩

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