prod_range_succ_factorial — Mathlib

English

For every natural number n, the product of the factorials 0!, 1!, ..., n! equals the super-factorial sf(n).

Русский

Для каждого натурального числа n произведение факториалов 0!, 1!, ..., n! равно sf(n).

LaTeX

$$$\prod_{x=0}^{n} x! = sf(n)$$$

Lean4

@[simp]
theorem prod_range_succ_factorial : ∀ n : ℕ, ∏ x ∈ range (n + 1), x ! = sf n
  | 0 => rfl
  | n + 1 => by rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]

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