Theorem: ArithmeticFunction.IsMultiplicative.prod_factors_of_mult (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

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