English
For all n,l,k ∈ ℕ, n^{\overline{l}} · (n+l)^{\overline{k}} = n^{\overline{l+k}}.
Русский
Для любых n,l,k ∈ ℕ: n^{\overline{l}} · (n+l)^{\overline{k}} = n^{\overline{l+k}}.
LaTeX
$$$$\forall n,l,k \in \mathbb{N},\ n^{\overline{l}} \cdot (n+l)^{\overline{k}} = n^{\overline{l+k}}$$$$
Lean4
theorem ascFactorial_mul_ascFactorial (n l k : ℕ) :
n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k) := by
cases n with
| zero =>
cases l
· simp only [ascFactorial_zero, Nat.add_zero, Nat.one_mul, Nat.zero_add]
· simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]
| succ n' =>
apply Nat.mul_left_cancel (factorial_pos n')
simp only [Nat.add_assoc, ← Nat.mul_assoc, factorial_mul_ascFactorial]
rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]
