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_prod_left {ι : Type u_1} {x : } {s : ι} {t : Finset ι} :
(it, 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 ι} :
(it, 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