ordinaryHypergeometric_zero — Mathlib

English

The ₂F₁ hypergeometric series evaluated at 0 is the identity element: equals 1.

Русский

Значение обыкновенного гипергеометрического ряда при аргументе 0 равно единице.

LaTeX

$$$₂F₁(a,b,c)\\big|_{x=0} = 1$$$

Lean4

@[simp]
theorem ordinaryHypergeometric_zero : ₂F₁ a b c (0 : 𝔸) = 1 := by
  simp [ordinaryHypergeometric_eq_tsum, ← ordinaryHypergeometricSeries_apply_eq,
    ordinaryHypergeometricSeries_apply_zero]

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