Gamma_mul_Gamma_one_sub — Mathlib

English

For real s, Gamma(s) Gamma(1 − s) = π / sin(π s).

Русский

Для действительного s: Gamma(s) Gamma(1 − s) = π / sin(π s).

LaTeX

$$$$ \Gamma(s) \Gamma(1 - s) = \frac{\pi}{\sin(\pi s)}. $$$$

Lean4

/-- Euler's reflection formula for the real Gamma function. -/
theorem Gamma_mul_Gamma_one_sub (s : ℝ) : Gamma s * Gamma (1 - s) = π / sin (π * s) :=
  by
  simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.ofReal_sin, Complex.ofReal_mul, ← Complex.Gamma_ofReal,
    Complex.ofReal_sub, Complex.ofReal_one]
  exact Complex.Gamma_mul_Gamma_one_sub s

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