factorial_mul_ascFactorial' — Mathlib

English

If n > 0, (n-1)! · n^{\overline{k}} = (n+k-1)!.

Русский

Пусть n > 0. Тогда (n-1)! · n^{\overline{k}} = (n+k-1)!.

LaTeX

$$$$\forall n,k \in \mathbb{N}, n>0 \Rightarrow (n-1)! \cdot n^{\overline{k}} = (n+k-1)!$$$$

Lean4

/-- `n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See
`Nat.ascFactorial_eq_div` for the version with ℕ-division. Consider using
`factorial_mul_ascFactorial` to avoid complications of ℕ-subtraction. -/
theorem factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) : (n - 1)! * n.ascFactorial k = (n + k - 1)! :=
  by
  rw [Nat.sub_add_comm h, Nat.sub_one]
  nth_rw 2 [Nat.eq_add_of_sub_eq h rfl]
  rw [Nat.sub_one, factorial_mul_ascFactorial]

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