ordinaryHypergeometric_radius_top_of_neg_nat₂

English

The radius result extends to the symmetric case with neg nat parameter on a and c.

Русский

Радиусной результат распространяется на симметричный случай с отрицательным натуральным параметром a и c.

LaTeX

$$$\\text{radius}(\\ordinaryHypergeometricSeries(a, -k, c)) = \\top$$$

Lean4

theorem ordinaryHypergeometric_radius_top_of_neg_nat₂ {k : ℕ} :
    (ordinaryHypergeometricSeries 𝔸 a (-(k : 𝕂)) c).radius = ⊤ :=
  by
  rw [ordinaryHypergeometricSeries_symm]
  exact ordinaryHypergeometric_radius_top_of_neg_nat₁ 𝔸 a c

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