no goals
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
⊢ a ^ 0 ∣ b ^ 0
rw [pow_zero, pow_zero]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a * a ^ n ∣ b * b ^ n
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a ^ (n + 1) ∣ b ^ (n + 1)
rw [pow_succ, pow_succ]
no goals
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a * a ^ n ∣ b * b ^ n
exact mul_dvd_mul h (pow_dvd_pow_of_dvd h n)