English
The binomial coefficient equals the product over primes p of p raised to the exponent (choose n k).factorization p.
Русский
Биномальный коэффициент равен произведению по всем простым p от p в степени (n choose k).factorization p.
LaTeX
$$$ \\prod_{p \\in \\mathrm{range}(n+1)} p^{\\ (n\\choose k).factorization p} = \\binom{n}{k}. $$$
Lean4
/-- A binomial coefficient is the product of its prime factors, which are at most `n`. -/
theorem prod_pow_factorization_choose (n k : ℕ) (hkn : k ≤ n) :
(∏ p ∈ Finset.range (n + 1), p ^ (Nat.choose n k).factorization p) = choose n k :=
by
conv_rhs => rw [← factorization_prod_pow_eq_self (choose_ne_zero hkn)]
rw [eq_comm]
apply Finset.prod_subset
· intro p hp
rw [Finset.mem_range]
contrapose! hp
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
· intro p _ h2
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]
