one_div_Gamma_eq_self_mul_one_div_Gamma_add_one

English

For all s ∈ ℂ, (Γ(s))^{-1} = s (Γ(s+1))^{-1}.

Русский

Для всех s ∈ ℂ: (Γ(s))^{-1} = s (Γ(s+1))^{-1}.

LaTeX

$$$$ \Gamma(s)^{-1} = s \cdot \Gamma(s+1)^{-1}. $$$$

Lean4

/-- A reformulation of the Gamma recurrence relation which is true for `s = 0` as well. -/
theorem one_div_Gamma_eq_self_mul_one_div_Gamma_add_one (s : ℂ) : (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹ :=
  by
  rcases ne_or_eq s 0 with (h | rfl)
  · rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]
  · rw [zero_add, Gamma_zero, inv_zero, zero_mul]

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