LeanPool.SelbergSieve4.ForMathlib.Basic

theorem Aux.mult_lcm_eq_of_ne_zero {R : Type u_1} [CommGroupWithZero R] (f : ArithmeticFunction R) (h_mult : f.IsMultiplicative) (x y : ℕ) (hf : f (x.gcd y) ≠ 0) : f (x.lcm y) = f x * f y / f (x.gcd y)

theorem Aux.prod_factors_of_mult (f : ArithmeticFunction ℝ) (h_mult : f.IsMultiplicative) {l : ℕ} (hl : Squarefree l) : ∏ a ∈ l.primeFactors, f a = f l