no goals
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
⊢ x ∣ y ^ n ↔ x ∣ y
classical
  haveI := UniqueFactorizationMonoid.toGCDMonoid R
  exact ⟨hsq.isRadical n y, fun h => h.pow h0⟩
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
this : GCDMonoid R
⊢ x ∣ y ^ n ↔ x ∣ y
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
⊢ x ∣ y ^ n ↔ x ∣ y
haveI := UniqueFactorizationMonoid.toGCDMonoid R
no goals
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
this : GCDMonoid R
⊢ x ∣ y ^ n ↔ x ∣ y
exact ⟨hsq.isRadical n y, fun h => h.pow h0⟩