unfold selbergTerms
s : Sieve
d : ℕ
⊢ g d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
s : Sieve
d : ℕ
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)