prod_Icc_factorial — Mathlib

English

For all n, the product of x! over x in Icc 1 n equals sf n.

Русский

Для всех n произведение x! по x ∈ Icc 1 n равно sf n.

LaTeX

$$$ \prod_{x \in \mathrm{Icc}(1,n)} x! = \mathrm{sf}(n) $$$

Lean4

@[simp]
theorem prod_Icc_factorial : ∀ n : ℕ, ∏ x ∈ Icc 1 n, x ! = sf n
  | 0 => rfl
  | n + 1 => by
    rw [← Ico_add_one_right_eq_Icc 1, prod_Ico_succ_top le_add_self, Nat.factorial_succ, Ico_add_one_right_eq_Icc 1 n,
      prod_Icc_factorial n, superFactorial, factorial, mul_comm]

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