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 : ι), 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 : ι), 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