R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ ↑{ toFun := fun x => ↑f x ^ k, map_zero' := (_ : (fun x => ↑f x ^ k) 0 = 0) } x = ↑f x ^ k
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ ↑(ppow f k) x = ↑f x ^ k
rw [ppow, dif_neg (ne_of_gt kpos)]
no goals
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ ↑{ toFun := fun x => ↑f x ^ k, map_zero' := (_ : (fun x => ↑f x ^ k) 0 = 0) } x = ↑f x ^ k
rfl