primorial_add_dvd — Mathlib

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)

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