no goals
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
⊢ IsCoprime x (∏ i in t, s i) ↔ ∀ (i : I), i ∈ t → IsCoprime x (s i)
simpa only [isCoprime_comm] using IsCoprime.prod_left_iff (R := R)