English
Let n ∈ ℕ. The central binomial coefficient C(2n, n) equals the product over primes p ≤ 2n of p raised to the exponent of p in the prime factorization of C(2n, n). Equivalently, ∏_{p ≤ 2n} ν_p(C(2n,n)) is the exponent of p in C(2n,n), and ∏_{p ≤ 2n} p^{ν_p(C(2n,n))} = C(2n,n).
Русский
Пусть n ∈ ℕ. Центральный биномиальный коэффициент C(2n, n) равен произведению по всем простым p ≤ 2n степени p, равной степени p в разложении C(2n,n). Эквивалентно, ∏_{p ≤ 2n} p^{ν_p(C(2n,n))} = C(2n,n).
LaTeX
$$$ \\prod_{p \\le 2n} p^{\\nu_p\\left(\\binom{2n}{n}\\right)} = \\binom{2n}{n} $$$
Lean4
/-- The `n`th central binomial coefficient is the product of its prime factors, which are
at most `2n`. -/
theorem prod_pow_factorization_centralBinom (n : ℕ) :
(∏ p ∈ Finset.range (2 * n + 1), p ^ (centralBinom n).factorization p) = centralBinom n :=
by
apply prod_pow_factorization_choose
cutsat
