case h
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
n : ℕ
⊢ ↑↑(f * g) n = ↑(↑f * ↑g) n
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
⊢ ↑(f * g) = ↑f * ↑g
ext n
no goals
case h
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
n : ℕ
⊢ ↑↑(f * g) n = ↑(↑f * ↑g) n
simp