superFactorial_two_mul — Mathlib

English

For every n, sf(2n) equals the square of the product of odd factorials up to (2n−1), multiplied by 2^n and by n!.

Русский

Для любого n верно: sf(2n) = (∏_{i=0}^{n-1} (2i+1)!)^2 · 2^n · n!.

LaTeX

$$$ sf(2n) = \left( \prod_{i=0}^{n-1} (2i+1)! \right)^2 \cdot 2^n \cdot n!$$$

Lean4

theorem superFactorial_two_mul : ∀ n : ℕ, sf(2 * n) = (∏ i ∈ range n, (2 * i + 1)!) ^ 2 * 2 ^ n * n !
  | 0 => rfl
  | (n + 1) =>
    by
    simp only [prod_range_succ, mul_pow, mul_add, mul_one, superFactorial_succ, superFactorial_two_mul n,
      factorial_succ]
    ring

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