descFactorial_succ

Mathlib.Data.Nat.Factorial.Basic

URI: https://scilib.ai/kg/mathlib#Nat.descFactorial_succ

English

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

Русский

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

LaTeX

$$$$\operatorname{descFactorial}(n,k+1) = (n-k) \cdot \operatorname{descFactorial}(n,k)$$$$

Lean4

@[simp]
theorem descFactorial_succ (n k : ℕ) : n.descFactorial (k + 1) = (n - k) * n.descFactorial k :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru