simp_rw [pdiv_apply, hf.2, hg.2]
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ (f.pdiv g) (a * b) = (f.pdiv g) a * (f.pdiv g) b
case right
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
a b : ℕ
⊢ f a * f b / (g a * g b) = f a / g a * (f b / g b)