primorial_add — Mathlib

English

The primorial of m+n equals m# times the product of primes in the interval (m, m+n].

Русский

Примориал (m+n) равен произведению m# и произведению простых в интервале (m, m+n].

LaTeX

$$$(m+n)\# = m\# \cdot \prod_{p \in Ico(m+1, m+n+1)} p \text{ with } p,\, p\text{ Prime}$$$

Lean4

theorem primorial_add (m n : ℕ) : (m + n)# = m# * ∏ p ∈ Ico (m + 1) (m + n + 1) with p.Prime, p :=
  by
  rw [primorial, primorial, ← Ico_zero_eq_range, ← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
  exacts [Nat.zero_le _, add_le_add_right (Nat.le_add_right _ _) _,
    disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]

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