lean_workbook_plus_58008
ProvedProve that there exists a number such that are not divisible by for all given a set of finite primes and numbers which are not divisible by any .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58008 (P : Finset ℕ) (n : ℕ → ℕ) (hP : ∀ p ∈ P, p.Prime) (hn : ∀ r, ¬ ∃ p ∈ P, p ∣ n r) : ∃ t, ∀ p ∈ P, ¬ p ∣ t + n 0 := by sorry
Source