[`Analysis/SpecialFunctions/Gamma/Beta`] `Γ(s - 1) = Γ(s + 1)` iff

[SnirBroshi]

• Complex.Gamma (s - 1/2) = Complex.Gamma (s + 1/2) ↔ s = 3/2 ∨ ∃ n : ℕ, s = -n - 1/2
  Mentioned on Wikipedia.
  Follows easily from Complex.Gamma_mul_Gamma_add_half twice and Complex.Gamma_add_one and Complex.Gamma_eq_zero_iff.

• Complex.Gamma (s - 1) = Complex.Gamma (s + 1) ↔ s ∈ { φ, ψ }
  Mentioned on Wikipedia twice.
  Probably 4 usages of Gamma_mul_Gamma_add_half.