mathlib documentation

data.nat.gcd.big_operators

Lemmas about coprimality with big products. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (s i).coprime x) (t.prod (λ (i : ι), s i)).coprime x

See is_coprime.prod_left for the corresponding lemma about is_coprime

theorem nat.coprime_prod_right {ι : Type u_1} {x : } {s : ι } {t : finset ι} :
( (i : ι), i t x.coprime (s i)) x.coprime (t.prod (λ (i : ι), s i))

See is_coprime.prod_right for the corresponding lemma about is_coprime