English
For all 𝔸, a, b, c in 𝕂 and n in ℕ, the nth term of the ordinary hypergeometric series vanishes iff there exists a natural k < n with k = -a or k = -b or k = -c (after casting to 𝕂).
Русский
Для любых 𝔸, a, b, c ∈ 𝕂 и n ∈ ℕ н-ая член обыкновенной гипергеометрической серии равен нулю тогда и только тогда, когда существует натуральное k < n, такое что k = -a или k = -b или k = -c (после приведения к 𝕂).
LaTeX
$$$$ \mathrm{ordinaryHypergeometricSeries} \; \mathbb{A} \ a \ b \ c \ n = 0 \iff \exists k < n,\; k = -a \lor k = -b \lor k = -c. $$$$
Lean4
/-- An iff variation on `ordinaryHypergeometricSeries_eq_zero_of_nonpos_int` for `[RCLike 𝕂]`. -/
theorem ordinaryHypergeometricSeries_eq_zero_iff (n : ℕ) :
ordinaryHypergeometricSeries 𝔸 a b c n = 0 ↔ ∃ k < n, k = -a ∨ k = -b ∨ k = -c :=
by
refine ⟨fun h ↦ ?_, fun zero ↦ ?_⟩
· rw [ordinaryHypergeometricSeries, ofScalars_eq_zero] at h
simp only [_root_.mul_eq_zero, inv_eq_zero] at h
rcases h with ((hn | h) | h) | h
· simp [Nat.factorial_ne_zero] at hn
all_goals
obtain ⟨kn, hkn, hn⟩ := (ascPochhammer_eval_eq_zero_iff _ _).1 h
exact ⟨kn, hkn, by tauto⟩
· obtain ⟨_, h, hn⟩ := zero
exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat a b c hn h
