descFactorial_eq_prod_range

Mathlib.Data.Nat.Factorial.BigOperators

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

← MathLib Explorer

English

For all n and k, n.descFactorial k equals the product over i in range k of (n−i).

Русский

Для всех n,k: n↓k = ∏_{i=0}^{k-1} (n−i).

LaTeX

$$n.descFactorial k = ∏_{i ∈ range k} (n - i)$$

Lean4

theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i ∈ range k, (n - i)
  | 0 => rfl
  | k + 1 => by rw [descFactorial, prod_range_succ_comm, descFactorial_eq_prod_range n k]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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