ascPochhammer_ne_zero_eval_zero

Mathlib.RingTheory.Polynomial.Pochhammer

URI: https://scilib.ai/kg/mathlib#ascPochhammer_ne_zero_eval_zero

English

If n ≠ 0, then ascPochhammer S n evaluates to 0 at 0.

Русский

Если n ≠ 0, то ascPochhammer S n в 0 даёт 0.

LaTeX

$$$(ascPochhammer S n).\\mathrm{eval} 0 = 0 \\quad\\text{если } n \\neq 0$$$

Lean4

@[simp]
theorem ascPochhammer_ne_zero_eval_zero {n : ℕ} (h : n ≠ 0) : (ascPochhammer S n).eval 0 = 0 := by
  simp [ascPochhammer_eval_zero, h]

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

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

Разделы

Аффилиация

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