descPochhammer_eval_coe_nat_of_lt

English

For natural k,n, (descPochhammer R n).eval (k : R) = 0 whenever k < n.

Русский

Для натуральных k,n: (descPochhammer R n).eval(k) = 0, если k < n.

LaTeX

$$$\text{If } k

Lean4

/-- `descPochhammer R n` is `0` for `0, 1, …, n-1`. -/
theorem descPochhammer_eval_coe_nat_of_lt {k n : ℕ} (h : k < n) : (descPochhammer R n).eval (k : R) = 0 :=
  by
  rw [descPochhammer_eval_eq_ascPochhammer, sub_add_eq_add_sub, ← Nat.cast_add_one, ← neg_sub, ← Nat.cast_sub h]
  exact ascPochhammer_eval_neg_coe_nat_of_lt (Nat.sub_lt_of_pos_le k.succ_pos h)

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