succ_descFactorial — Mathlib

English

(n+1 - k) · (n+1).descFactorial k = (n+1) · n.descFactorial k.

Русский

(n+1 - k) · (n+1).descFactorial k = (n+1) · n.descFactorial k.

LaTeX

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

Lean4

theorem succ_descFactorial (n : ℕ) : ∀ k, (n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
  | 0 => by rw [Nat.sub_zero, descFactorial_zero, descFactorial_zero]
  | k + 1 => by rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, Nat.mul_left_comm]

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