Lemmas about coprimality with big products. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

These lemmas are kept separate from data.nat.gcd.basic in order to minimize imports.

theorem nat.coprime_prod_left {ι : Type u_1} {x : ℕ} {s : ι → ℕ} {t : finset ι} :

(∀ (i : ι), i ∈ t → (s i).coprime x) → (t.prod (λ (i : ι), s i)).coprime x

See is_coprime.prod_left for the corresponding lemma about is_coprime

theorem nat.coprime_prod_right {ι : Type u_1} {x : ℕ} {s : ι → ℕ} {t : finset ι} :

(∀ (i : ι), i ∈ t → x.coprime (s i)) → x.coprime (t.prod (λ (i : ι), s i))

See is_coprime.prod_right for the corresponding lemma about is_coprime