Gamma_zero

Mathlib.Analysis.SpecialFunctions.Gamma.Basic

URI: https://scilib.ai/kg/mathlib#Real.Gamma_zero

← MathLib Explorer

English

By convention, the Gamma function at 0 is defined to be 0: Γ(0) = 0.

Русский

По соглашению Γ(0) = 0.

LaTeX

$$$\Gamma(0) = 0$$$

Lean4

/-- At `0` the Gamma function is undefined; by convention we assign it the value `0`. -/
@[simp]
theorem Gamma_zero : Gamma 0 = 0 := by
  simpa only [← Complex.ofReal_zero, Complex.Gamma_ofReal, Complex.ofReal_inj] using Complex.Gamma_zero

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru