have hd_pos : 0 < d := Nat.pos_of_ne_zero $ ne_zero_of_dvd_ne_zero s.prodPrimes_ne_zero hdP
case a
s : Sieve
d : ℕ
hdP : d ∣ P
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹
case a
s : Sieve
d : ℕ
hdP : d ∣ P
hd_pos : 0 < d
⊢ ∑ a ∈ d.divisors, 1 / g a = (ν d)⁻¹