doubleFactorial_eq_prod_even — Mathlib

English

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

Русский

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

LaTeX

$$$ (2n)‼ = \prod_{i=1}^{n} 2i $$$

Lean4

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

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