α : Type u_1
β : Type ?u.38286
γ : Type ?u.38289
δ : Type ?u.38292
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a
α : Type u_1
β : Type ?u.38286
γ : Type ?u.38289
δ : Type ?u.38292
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ a * b
⊢ p ^ n ∣ a
rw [mul_comm] at h'
no goals
α : Type u_1
β : Type ?u.38286
γ : Type ?u.38289
δ : Type ?u.38292
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
n : ℕ
h : ¬p ∣ b
h' : p ^ n ∣ b * a
⊢ p ^ n ∣ a
exact hp.pow_dvd_of_dvd_mul_left n h h'