smeval_ascPochhammer_neg_of_lt

Mathlib.RingTheory.Binomial

URI: https://scilib.ai/kg/mathlib#Ring.smeval_ascPochhammer_neg_of_lt

← MathLib Explorer

English

If n < k then smeval(ascPochhammer ℕ k) evaluated at -n equals 0.

Русский

Если n < k, то smeval(ascPochhammer ℕ k)(-n) = 0.

LaTeX

$$$n

Lean4

@[simp]
theorem smeval_ascPochhammer_neg_of_lt {n k : ℕ} (h : n < k) : smeval (ascPochhammer ℕ k) (-n : ℤ) = 0 := by
  rw [show k = n + (k - n - 1) + 1 by cutsat, smeval_ascPochhammer_neg_add]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru