rw [mul_sum]
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∑ d ∈ l.divisors, ↑(μ d) * ν d = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ ∑ i ∈ l.divisors, (ν l)⁻¹ * (↑(μ i) * ν i) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹