doubleFactorial_eq_prod_odd — Mathlib

English

For all n, (2n+1)‼ equals the product ∏_{i=0}^{n-1} (2(i+1)+1).

Русский

Для всех n: (2n+1)‼ равно произведению ∏_{i=0}^{n-1} (2(i+1)+1).

LaTeX

$$$ (2n+1)‼ = \prod_{i\in \mathrm{range}(n)} (2(i+1)+1) $$$

Lean4

theorem doubleFactorial_eq_prod_odd : ∀ n : ℕ, (2 * n + 1)‼ = ∏ i ∈ Finset.range n, (2 * (i + 1) + 1)
  | 0 => rfl
  | n + 1 =>
    by
    rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
      (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]
    rfl

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