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 : ℕ} : Nat.Coprime (List.prod l) k ↔ ∀ n ∈ l, Nat.Coprime n k

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

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

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

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

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

theorem Nat.Coprime.prod_left {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ} : (∀ i ∈ t, Nat.Coprime (s i) x) → Nat.Coprime (Finset.prod t fun (i : ι) => s i) 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, Nat.Coprime x (s i)) → Nat.Coprime x (Finset.prod t 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 : ℕ} : Nat.Coprime (Finset.prod Finset.univ fun (i : ι) => s i) x ↔ ∀ (i : ι), Nat.Coprime (s i) x

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