Gammaℝ_eq_zero_iff — Mathlib

English

Γℝ s = 0 if and only if s = −2n for some n ∈ ℕ.

Русский

Γℝ(s) = 0 тогда и только тогда, когда существует n ∈ ℕ такое, что s = −2n.

LaTeX

$$$ \Gamma\mathbb{R}(s) = 0 \;\;\iff\;\; \exists n \in \mathbb{N},\; s = -(2n) $$$

Lean4

theorem Gammaℝ_eq_zero_iff {s : ℂ} : Gammaℝ s = 0 ↔ ∃ n : ℕ, s = -(2 * n) := by
  simp [Gammaℝ_def, Complex.Gamma_eq_zero_iff, pi_ne_zero, div_eq_iff (two_ne_zero' ℂ), mul_comm]

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