ascPochhammer_nat_eq_ascFactorial

English

For natural numbers n and k, (ascPochhammer Nat k).eval n = n ascFactorial k.

Русский

Для натуральных чисел n и k: (ascPochhammer Nat k).eval n = n ascFactorial k.

LaTeX

$$$\\forall n,k:\\ (ascPochhammer\\ Nat\\ k).\\mathrm{eval}\\ n = n.\\mathrm{ascFactorial}\\ k$$$

Lean4

theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) : ∀ k, (ascPochhammer ℕ k).eval n = n.ascFactorial k
  | 0 => by rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]
  | t + 1 => by
    rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X, eval_natCast,
      Nat.cast_id, Nat.ascFactorial_succ, mul_comm]

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