SelbergSieve.conv_selbergTerms_eq_selbergTerms_mul_nu

theorem conv_selbergTerms_eq_selbergTerms_mul_nu {d : ℕ} (hd : d ∣ P) :    (∑ l ∈ divisors P, if l ∣ d then g l else 0) = g d * (ν d)⁻¹ := by  calc    (∑ l ∈ divisors P, if l ∣ d then g l else 0) =        ∑ l ∈ divisors P, if l ∣ d then g (d / l) else 0 := by      rw [← sum_over_dvd_ite prodPrimes_ne_zero hd,        ← Nat.sum_divisorsAntidiagonal fun x _ => g x,        Nat.sum_divisorsAntidiagonal' fun x _ => g x, sum_over_dvd_ite prodPrimes_ne_zero hd]    _ = g d * ∑ l ∈ divisors P, if l ∣ d then 1 / g l else 0 := by      rw [mul_sum]; apply sum_congr rfl; intro l hl      rw [mul_ite_zero]; apply if_ctx_congr Iff.rfl _ (fun _ => rfl); intro h      rw [← div_mult_of_dvd_squarefree g (selbergTerms_mult s) d l h]      · ring      · apply Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree      · apply _root_.ne_of_gt; rw [mem_divisors] at hl; apply selbergTerms_pos; exact hl.left    _ = g d * (ν d)⁻¹ := by rw [← nu_eq_conv_one_div_selbergTerms s d hd]