English
Gamma(s) ≠ 0 whenever s ≠ −m for every m ∈ ℕ.
Русский
Gamma(s) ≠ 0 тогда, когда s ≠ −m для любого m ∈ ℕ.
LaTeX
$$$$ \forall s \in \mathbb{C}, \; \bigl( \forall m \in \mathbb{N}, \; s \neq -m \bigr) \Rightarrow \Gamma(s) \neq 0. $$$$
Lean4
/-- The Gamma function does not vanish on `ℂ` (except at non-positive integers, where the function
is mathematically undefined and we set it to `0` by convention). -/
theorem Gamma_ne_zero {s : ℂ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 :=
by
by_cases h_im : s.im = 0
· have : s = ↑s.re := by
conv_lhs => rw [← Complex.re_add_im s]
rw [h_im, ofReal_zero, zero_mul, add_zero]
rw [this, Gamma_ofReal, ofReal_ne_zero]
refine Real.Gamma_ne_zero fun n => ?_
specialize hs n
contrapose! hs
rwa [this, ← ofReal_natCast, ← ofReal_neg, ofReal_inj]
· have : sin (↑π * s) ≠ 0 := by
rw [Complex.sin_ne_zero_iff]
intro k
apply_fun im
rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]
exact mul_ne_zero Real.pi_pos.ne' h_im
have A := div_ne_zero (ofReal_ne_zero.mpr Real.pi_pos.ne') this
rw [← Complex.Gamma_mul_Gamma_one_sub s, mul_ne_zero_iff] at A
exact A.1
