R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y
refine' ⟨fun h ↦ _, IsCoprime.pow_left⟩
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
h : IsCoprime (∏ _x in range m, x) y
⊢ IsCoprime x y
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y
rw [← Finset.card_range m, ← Finset.prod_const] at h
no goals
R : Type u
I : Type v
inst✝ : CommSemiring R
x y z : R
s : I → R
t : Finset I
m n : ℕ
hm : 0 < m
h : IsCoprime (∏ _x in range m, x) y
⊢ IsCoprime x y
exact h.of_prod_left 0 (Finset.mem_range.mpr hm)