constructor
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ CompletelyMultiplicative (f.pdiv g)
case left
f g : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hg : CompletelyMultiplicative g
⊢ (f.pdiv g) 1 = 1

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