Gamma_ofReal — Mathlib

English

If s is a real number, the complex Gamma at s agrees with the real Gamma value, i.e., Γ(s) considered in the complex plane equals the real-valued Γ(s).

Русский

Если s — число действительное, то комплексная гамма в точке s совпадает с вещественной гаммой, то есть Γ(s) как комплексное число равна вещественному значению Γ(s).

LaTeX

$$$\forall s\in\mathbb{R},\quad \Gamma(s) \;\text{(as a complex value)} = \Gamma(s)\,.$$$

Lean4

theorem _root_.Complex.Gamma_ofReal (s : ℝ) : Complex.Gamma (s : ℂ) = Gamma s := by
  rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]

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