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

m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k

k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n

theorem Nat.coprime_prod_left_iff {ι : Type u_1} {t : Finset ι} {s : ι → ℕ} {x : ℕ} :

(∏ i ∈ t, 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 (∏ i ∈ t, 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) → (∏ i ∈ t, 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 (∏ i ∈ t, 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 : ℕ} :

(∏ 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 (∏ i : ι, s i) ↔ ∀ (i : ι), x.Coprime (s i)

Documentation