R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x in range n, y)
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (y ^ n)
rw [← Finset.card_range n, ← Finset.prod_const]
no goals
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x in range n, y)
exact IsCoprime.prod_right fun _ _ ↦ H