Lemmas about coprimality with big products.

These lemmas are kept separate from Data.Nat.GCD.Basic in order to minimize imports.

theorem Nat.coprime_list_prod_left_iff {l : List ℕ} {k : ℕ} : l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k

theorem Nat.coprime_list_prod_right_iff {k : ℕ} {l : List ℕ} : k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n

theorem Nat.coprime_multiset_prod_left_iff {m : Multiset ℕ} {k : ℕ} : m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k

theorem Nat.coprime_multiset_prod_right_iff {k : ℕ} {m : Multiset ℕ} : k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n

theorem Nat.coprime_prod_left_iff {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ} : (t.prod fun (i : ι) => s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x

theorem Nat.coprime_prod_right_iff {ι : Type u_1} {x : ℕ} {t : Finset ι} {s : ι → ℕ} : x.Coprime (t.prod fun (i : ι) => s i) ↔ ∀ i ∈ t, x.Coprime (s i)

theorem Nat.Coprime.prod_left {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ} : (∀ i ∈ t, (s i).Coprime x) → (t.prod fun (i : ι) => s i).Coprime x

See IsCoprime.prod_left for the corresponding lemma about IsCoprime

theorem Nat.Coprime.prod_right {ι : Type u_1} {x : ℕ} {t : Finset ι} {s : ι → ℕ} : (∀ i ∈ t, x.Coprime (s i)) → x.Coprime (t.prod fun (i : ι) => s i)

See IsCoprime.prod_right for the corresponding lemma about IsCoprime

theorem Nat.coprime_fintype_prod_left_iff {ι : Type u_1} [Fintype ι] {s : ι → ℕ} {x : ℕ} : (Finset.univ.prod fun (i : ι) => s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x

theorem Nat.coprime_fintype_prod_right_iff {ι : Type u_1} [Fintype ι] {x : ℕ} {s : ι → ℕ} : x.Coprime (Finset.univ.prod fun (i : ι) => s i) ↔ ∀ (i : ι), x.Coprime (s i)