ascFactorial_eq_prod_range

Mathlib.Data.Nat.Factorial.BigOperators

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$n.ascFactorial k = ∏_{i ∈ range k} (n + i)$$

Lean4

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

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

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

Разделы

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

Аффилиация

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