Mathlib.Data.Nat.GCD.BigOperators

Nat.coprime_list_prod_left_iff theorem

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

Full source

theorem coprime_list_prod_left_iff {l : List ℕ} {k : ℕ} :
    CoprimeCoprime l.prod k ↔ ∀ n ∈ l, Coprime n k := by
  induction l <;> simp [Nat.coprime_mul_iff_left, *]

Coprimality Condition for Product of List Elements

Informal description

For any list $l$ of natural numbers and any natural number $k$, the product of the elements in $l$ is coprime with $k$ if and only if every element $n$ in $l$ is coprime with $k$. In other words: \[ \gcd\left(\prod_{n \in l} n, k\right) = 1 \leftrightarrow \forall n \in l, \gcd(n, k) = 1. \]

Nat.coprime_list_prod_right_iff theorem

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

Full source

theorem coprime_list_prod_right_iff {k : ℕ} {l : List ℕ} :
    CoprimeCoprime k l.prod ↔ ∀ n ∈ l, Coprime k n := by
  simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]

Coprimality with List Product (Right)

Informal description

For any natural number $k$ and list of natural numbers $l$, the number $k$ is coprime with the product of all elements in $l$ if and only if $k$ is coprime with every element $n$ in $l$.

Nat.coprime_multiset_prod_left_iff theorem

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

Full source

theorem coprime_multiset_prod_left_iff {m : Multiset ℕ} {k : ℕ} :
    CoprimeCoprime m.prod k ↔ ∀ n ∈ m, Coprime n k := by
  induction m using Quotient.inductionOn; simpa using coprime_list_prod_left_iff

Coprimality Condition for Product of Multiset Elements

Informal description

For any multiset $m$ of natural numbers and any natural number $k$, the product of the elements in $m$ is coprime with $k$ if and only if every element $n$ in $m$ is coprime with $k$. In other words: \[ \gcd\left(\prod_{n \in m} n, k\right) = 1 \leftrightarrow \forall n \in m, \gcd(n, k) = 1. \]

Nat.coprime_multiset_prod_right_iff theorem

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

Full source

theorem coprime_multiset_prod_right_iff {k : ℕ} {m : Multiset ℕ} :
    CoprimeCoprime k m.prod ↔ ∀ n ∈ m, Coprime k n := by
  induction m using Quotient.inductionOn; simpa using coprime_list_prod_right_iff

Coprimality with Multiset Product (Right)

Informal description

For any natural number $k$ and multiset of natural numbers $m$, the number $k$ is coprime with the product of all elements in $m$ if and only if $k$ is coprime with every element $n$ in $m$.

Nat.coprime_prod_left_iff theorem

{t : Finset ι} {s : ι → ℕ} {x : ℕ} : Coprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, Coprime (s i) x

Full source

theorem coprime_prod_left_iff {t : Finset ι} {s : ι → ℕ} {x : ℕ} :
    CoprimeCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, Coprime (s i) x := by
  simpa using coprime_multiset_prod_left_iff (m := t.val.map s)

Coprimality of Finite Product with Natural Number

Informal description

For any finite set $t$ indexed by $\iota$, a function $s : \iota \to \mathbb{N}$, and a natural number $x$, the product $\prod_{i \in t} s(i)$ is coprime with $x$ if and only if for every $i \in t$, $s(i)$ is coprime with $x$. In other words: \[ \gcd\left(\prod_{i \in t} s(i), x\right) = 1 \leftrightarrow \forall i \in t, \gcd(s(i), x) = 1. \]

Nat.coprime_prod_right_iff theorem

{x : ℕ} {t : Finset ι} {s : ι → ℕ} : Coprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, Coprime x (s i)

Full source

theorem coprime_prod_right_iff {x : ℕ} {t : Finset ι} {s : ι → ℕ} :
    CoprimeCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, Coprime x (s i) := by
  simpa using coprime_multiset_prod_right_iff (m := t.val.map s)

Coprimality with Finite Product: $x \perp \prod_{i \in t} s(i) \leftrightarrow \forall i \in t, x \perp s(i)$

Informal description

For any natural number $x$, finite set $t$ indexed by $\iota$, and function $s : \iota \to \mathbb{N}$, the number $x$ is coprime with the product $\prod_{i \in t} s(i)$ if and only if $x$ is coprime with $s(i)$ for every $i \in t$. In other words: \[ \gcd\left(x, \prod_{i \in t} s(i)\right) = 1 \leftrightarrow \forall i \in t, \gcd(x, s(i)) = 1. \]

Nat.coprime_fintype_prod_left_iff theorem

[Fintype ι] {s : ι → ℕ} {x : ℕ} : Coprime (∏ i, s i) x ↔ ∀ i, Coprime (s i) x

Full source

theorem coprime_fintype_prod_left_iff [Fintype ι] {s : ι → ℕ} {x : ℕ} :
    CoprimeCoprime (∏ i, s i) x ↔ ∀ i, Coprime (s i) x := by
  simp [coprime_prod_left_iff]

Coprimality of Product with Natural Number: $\gcd(\prod_i s(i), x) = 1 \leftrightarrow \forall i, \gcd(s(i), x) = 1$

Informal description

For a finite type $\iota$ and functions $s : \iota \to \mathbb{N}$ and $x \in \mathbb{N}$, the product $\prod_{i \in \iota} s(i)$ is coprime with $x$ if and only if for every $i \in \iota$, $s(i)$ is coprime with $x$. In other words: \[ \gcd\left(\prod_{i \in \iota} s(i), x\right) = 1 \leftrightarrow \forall i \in \iota, \gcd(s(i), x) = 1. \]

Nat.coprime_fintype_prod_right_iff theorem

[Fintype ι] {x : ℕ} {s : ι → ℕ} : Coprime x (∏ i, s i) ↔ ∀ i, Coprime x (s i)

Full source

theorem coprime_fintype_prod_right_iff [Fintype ι] {x : ℕ} {s : ι → ℕ} :
    CoprimeCoprime x (∏ i, s i) ↔ ∀ i, Coprime x (s i) := by
  simp [coprime_prod_right_iff]

Coprimality with Finite Product: $x \perp \prod_i s(i) \leftrightarrow \forall i, x \perp s(i)$

Informal description

Let $\iota$ be a finite type, $x$ a natural number, and $s : \iota \to \mathbb{N}$ a function. Then $x$ is coprime with the product $\prod_{i} s(i)$ if and only if $x$ is coprime with $s(i)$ for every $i \in \iota$.