English
For m,n with n ≤ m, (m+n)# divides m# times binomial(m+n, m).
Русский
При n ≤ m выполняется: (m+n)# делится на m# умноженное на биномиал(binomial(m+n, m)).
LaTeX
$$$(m+n)\# \mid m\# \cdot \binom{m+n}{m}$$$
Lean4
theorem primorial_add_dvd {m n : ℕ} (h : n ≤ m) : (m + n)# ∣ m# * choose (m + n) m :=
calc
(m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p := primorial_add _ _
_ ∣ m# * choose (m + n) m :=
mul_dvd_mul_left _ <|
prod_primes_dvd _ (fun _ hk ↦ (mem_filter.1 hk).2.prime) fun p hp ↦
by
rw [mem_filter, mem_Ico] at hp
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1)) (Nat.lt_succ_iff.1 hp.1.2)