rw [selbergTerms_apply]
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / g l = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / (ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹