Documentation

Mathlib.Data.Nat.GCD.BigOperators

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