ArithmeticFunction.two_pow_omega_LSeries_eulerProduct_hasProd

@[blueprint  "two_pow_omega_LSeries_eulerProduct_hasProd"  (title := "two-pow-omega-LSeries-eulerProduct-hasProd")  (statement := /--    For $1<\Re(s)$ we have that    $$\sum_{1\leq n}2^{\omega(n)}n^{-s}=\prod_p\frac{1+p^{-s}}{1-p^{-s}}.$$    The naming convention here is designed to match    \begin{verbatim}      riemannZeta_eulerProduct_hasProd    \end{verbatim}  -/)  (proof := /--    Immediately follows from Lemmas \ref{two-pow-omega-LSeries.term-IsMultiplicative} and \ref{two-pow-omega-tsum-prime-pow}.  -/)]lemma two_pow_omega_LSeries_eulerProduct_hasProd (s : ℂ) (hs : 1 < s.re) :    HasProd (fun (p : Primes) ↦ (1 + ↑↑p ^ (-s)) / (1 - ↑↑p ^ (-s))) (L (fun n ↦ (2 ^ ω n)) s) := by  convert! EulerProduct.eulerProduct_hasProd _ _ _ (LSeries.term_zero (fun n ↦ (2 ^ ω n)) s) using 1;  · funext p; exact Eq.symm (two_pow_omega_tsum_prime_pow hs p)  · simp only [ne_eq, one_ne_zero, not_false_eq_true, LSeries.term_of_ne_zero,      cardDistinctFactors_one, pow_zero, cast_one, Complex.one_cpow, div_self]  · intro _ _ mCn; exact two_pow_omega_LSeries.term_isMultiplicative s mCn  · convert! (LSeriesSummable_two_pow_omega hs).norm using 1