apply div_eq_of_eq_mul hd
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l / f d = f (l / d)
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l = f (l / d) * f d