Gammaℂ_add_one — Mathlib

English

For s ≠ 0, Γℂ(s+1) = Γℂ(s) · s / 2 / π.

Русский

Для s ≠ 0: Γℂ(s+1) = Γℂ(s) · s / (2π).

LaTeX

$$$ \Gamma\mathbb{C}(s+1) = \Gamma\mathbb{C}(s) \cdot \dfrac{s}{2 \pi} $$$

Lean4

theorem Gammaℂ_add_one {s : ℂ} (hs : s ≠ 0) : Gammaℂ (s + 1) = Gammaℂ s * s / 2 / π :=
  by
  rw [Gammaℂ_def, Gammaℂ_def, Gamma_add_one _ hs, neg_add,
    cpow_add _ _ (mul_ne_zero two_ne_zero (ofReal_ne_zero.mpr pi_ne_zero)), cpow_neg_one]
  field_simp

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