rw [←IsMultiplicative.map_prod_of_subset_primeFactors h_mult l _ Finset.Subset.rfl,
  Nat.prod_primeFactors_of_squarefree hl]
R : Type u_1
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
⊢ ∏ a ∈ l.primeFactors, f a = f l
no goals