smeval_ascPochhammer_neg_add — Mathlib

English

For all n,k ∈ ℕ, smeval of ascPochhammer at level (n+k+1) evaluated at -n equals 0.

Русский

Для всех n,k ∈ ℕ, вычисление smeval для ascPochhammer при уровне n+k+1 на -n даёт 0.

LaTeX

$$$\\forall n,k \\in \\mathbb{N},\\; \\operatorname{smeval}(\\ascPochhammer_{\\mathbb{N}}(n+k+1))(-n) = 0.$$$

Lean4

theorem smeval_ascPochhammer_neg_add (n : ℕ) : ∀ k : ℕ, smeval (ascPochhammer ℕ (n + k + 1)) (-n : ℤ) = 0
  | 0 => by rw [add_zero, smeval_ascPochhammer_succ_neg]
  | k + 1 => by rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k, zero_mul]

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