SelbergSieve.one_div_selbergTerms_eq_conv_moebius_nu

theorem one_div_selbergTerms_eq_conv_moebius_nu (l : ℕ) (hl : Squarefree l)    (hnu_nonzero : ν l ≠ 0) : 1 / g l = ∑ d ∈ l.divisors, (μ <| l / d) * (ν d)⁻¹ :=  by  rw [selbergTerms_apply]  simp only [one_div, prod_inv_distrib, mul_inv, inv_inv]  rw [(s.nu_mult).prodPrimeFactors_one_sub_of_squarefree _ hl]  rw [mul_sum]  apply symm  rw [← Nat.sum_divisorsAntidiagonal' fun d e : ℕ => ↑(μ d) * (ν e)⁻¹]  rw [Nat.sum_divisorsAntidiagonal fun d e : ℕ => ↑(μ d) * (ν e)⁻¹]  apply sum_congr rfl; intro d hd  have hd_dvd : d ∣ l := dvd_of_mem_divisors hd  rw [←div_mult_of_dvd_squarefree ν s.nu_mult l d (dvd_of_mem_divisors hd) hl, inv_div]  · ring  revert hnu_nonzero; contrapose!  exact multiplicative_zero_of_zero_dvd ν s.nu_mult hl hd_dvd