smeval_ascPochhammer_succ_neg — Mathlib

English

The smeval of the negated successive ascPochhammer satisfies a negation identity: smeval((ascPochhammer ℕ n).succ) at −m equals 0 for certain m and n.

Русский

Для смежной последовательности ascPochhammer существует нулевое свойство smeval при отрицательном аргументе.

LaTeX

$$$\mathrm{smeval}(\mathrm{ascPochhammer} ℕ n) (−m) = 0$$$

Lean4

@[simp]
theorem smeval_ascPochhammer_succ_neg (n : ℕ) : smeval (ascPochhammer ℕ (n + 1)) (-n : ℤ) = 0 := by
  rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C, pow_zero, pow_one,
    Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]

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