superFactorial_four_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem superFactorial_four_mul (n : ℕ) : sf(4 * n) = ((∏ i ∈ range (2 * n), (2 * i + 1)!) * 2 ^ n) ^ 2 * (2 * n)! :=
  calc
    sf(4 * n) = (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * 2 ^ (2 * n) * (2 * n)! := by
      rw [← superFactorial_two_mul, ← mul_assoc, Nat.mul_two]
    _ = ((∏ i ∈ range (2 * n), (2 * i + 1)!) * 2 ^ n) ^ 2 * (2 * n)! := by rw [pow_mul', mul_pow]

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