rw [mul_sum]
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = g d * ∑ l ∈ P.divisors, if l ∣ d then 1 / g l else 0
s : Sieve
d : ℕ
hd : d ∣ P
⊢ (∑ l ∈ P.divisors, if l ∣ d then g (d / l) else 0) = ∑ i ∈ P.divisors, g d * if i ∣ d then 1 / g i else 0