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 : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x in t, s x) x
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 : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
⊢ IsCoprime (∏ i in insert b t, s i) x
rw [Finset.prod_insert hbt]
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 : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : IsCoprime (s b) x ∧ ∀ (x_1 : I), x_1 ∈ t → IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x in t, s x) x
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 : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : ∀ (i : I), i ∈ insert b t → IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x in t, s x) x
rw [Finset.forall_mem_insert] at H
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 : (∀ (i : I), i ∈ t → IsCoprime (s i) x) → IsCoprime (∏ i in t, s i) x
H : IsCoprime (s b) x ∧ ∀ (x_1 : I), x_1 ∈ t → IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x in t, s x) x
exact H.1.mul_left (ih H.2)