no goals
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
x✝ : I
⊢ x✝ ∈ ∅ → IsCoprime (s x✝) x
simp
no goals
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : ¬b ∈ t
ih : IsCoprime (∏ i in t, s i) x ↔ ∀ (i : I), i ∈ t → IsCoprime (s i) x
⊢ IsCoprime (∏ i in insert b t, s i) x ↔ ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]