Lemmas about coprimality with big products. #
These lemmas are kept separate from Data.Nat.GCD.Basic in order to minimize imports.
theorem
Nat.coprime_prod_left
{ι : Type u_1}
{x : ℕ}
{s : ι → ℕ}
{t : Finset ι}
:
(∀ 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 : ℕ}
{s : ι → ℕ}
{t : Finset ι}
:
(∀ 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