prod_Ico_id_eq_factorial — Mathlib

English

Recursive relation for factorial: product over Ico(1, n+1) equals n!; with factorial step, (n+1)! = (n+1)·n!.

Русский

Рекурсивное соотношение для факториала.

LaTeX

$$$$ \\displaystyle \\text{(as above)} $$$$

Lean4

@[simp]
theorem prod_Ico_id_eq_factorial : ∀ n : ℕ, (∏ x ∈ Ico 1 (n + 1), x) = n !
  | 0 => rfl
  | n + 1 => by
    rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ, prod_Ico_id_eq_factorial n,
      Nat.succ_eq_add_one, mul_comm]

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