# 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 : } {k : } :
l.prod.Coprime k nl, n.Coprime k
theorem Nat.coprime_list_prod_right_iff {k : } {l : } :
k.Coprime l.prod nl, k.Coprime n
theorem Nat.coprime_multiset_prod_left_iff {m : } {k : } :
m.prod.Coprime k nm, n.Coprime k
theorem Nat.coprime_multiset_prod_right_iff {k : } {m : } :
k.Coprime m.prod nm, k.Coprime n
theorem Nat.coprime_prod_left_iff {ι : Type u_1} {t : } {s : ι} {x : } :
(t.prod fun (i : ι) => s i).Coprime x it, (s i).Coprime x
theorem Nat.coprime_prod_right_iff {ι : Type u_1} {x : } {t : } {s : ι} :
x.Coprime (t.prod fun (i : ι) => s i) it, x.Coprime (s i)
theorem Nat.Coprime.prod_left {ι : Type u_1} {t : } {s : ι} {x : } :
(it, (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 : } {s : ι} :
(it, 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} [] {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} [] {x : } {s : ι} :
x.Coprime (Finset.univ.prod fun (i : ι) => s i) ∀ (i : ι), x.Coprime (s i)