succ_descFactorial_succ — Mathlib

English

succ_descFactorial(n,k) : (n+1).descFactorial (k+1) = (n+1) · n.descFactorial k.

Русский

succ_descFactorial(n,k) : (n+1).descFactorial (k+1) = (n+1) · n.descFactorial k.

LaTeX

$$$$\forall n,k \in \mathbb{N},\ \operatorname{succ\_descFactorial}(n,k): (n+1) \descFactorial (k+1) = (n+1) \cdot n \descFactorial k$$$$

Lean4

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

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