Generic distribution lemmas

Finite lemmas connecting the multiples of a modulus in an additive sieve support to prime-counting congruences, and the coprimality characterization used to identify sieve remainders.

theorem AnalyticNumberTheory.Sieve.coprime_prod_iff_no_prime_dvd {P a : ℕ} : P.Coprime a ↔ ∀ (r : ℕ), Nat.Prime r → r ∣ P → ¬r ∣ a

A natural is coprime to a product exactly when no prime divisor of the product divides it.

theorem AnalyticNumberTheory.Sieve.prime_dvd_complement_iff_modEq {N p d : ℕ} (hp_lt : p < N) : d ∣ N - p ↔ p ≡ N [MOD d]

For p < N, divisibility d ∣ N - p is the congruence p ≡ N [MOD d].