α : Type ?u.250626
β : Type ?u.250629
γ : Type ?u.250632
δ : Type ?u.250635
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h✝ : p₁ ^ k₁ = p₂ ^ k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
α : Type ?u.250626
β : Type ?u.250629
γ : Type ?u.250632
δ : Type ?u.250635
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂
rw [← associated_iff_eq] at h⊢
no goals
α : Type ?u.250626
β : Type ?u.250629
γ : Type ?u.250632
δ : Type ?u.250635
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : Unique Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h✝ : p₁ ^ k₁ = p₂ ^ k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁