succ_ascFactorial — Mathlib

English

For all n,k ∈ ℕ, n · (n+1)^{\overline{k}} = (n+k) · n^{\overline{k}}.

Русский

Для всех n,k ∈ ℕ выполняется: n · (n+1)^{\overline{k}} = (n+k) · n^{\overline{k}}.

LaTeX

$$$$\forall n,k \in \mathbb{N},\ n \cdot (n+1)^{\overline{k}} = (n+k) \cdot n^{\overline{k}}$$$$

Lean4

theorem succ_ascFactorial (n : ℕ) : ∀ k, n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
  | 0 => by rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]
  | k + 1 => by rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add, ← Nat.add_assoc]

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