ascPochhammer_eval_neg_coe_nat_of_lt

English

The right successor identity: descPochhammer R (n+1) equals descPochhammer R n times (X − cast n).

Русский

Правило перехода справа: descPochhammer R (n+1) = descPochhammer R n · (X − n).

LaTeX

$$$\operatorname{descPochhammer}_R(n+1) = \operatorname{descPochhammer}_R(n) \cdot (X - n)$$$

Lean4

/-- The Pochhammer polynomial of degree `n` has roots at `0`, `-1`, ..., `-(n - 1)`. -/
theorem ascPochhammer_eval_neg_coe_nat_of_lt {n k : ℕ} (h : k < n) : (ascPochhammer R n).eval (-(k : R)) = 0 := by
  induction n with
  | zero => contradiction
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · cutsat

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