LSeries d eq riemann Zeta pow

@[blueprint  "LSeries_d_eq_riemannZeta_pow"  (title := "LSeries d eq riemannZeta pow")  (statement := /-- The $L$-series of $d_k$ equals $\zeta(s)^k$ for $\Re(s) > 1$. -/)  (proof := /--  From the definition of $d_k$ as the $k$-fold Dirichlet convolution of $\zeta$, we can express $d_k$ as $\zeta^k$. The L-series of a Dirichlet convolution corresponds to the product of the L-series of the individual functions. Since $L(\zeta, s)$ is the Riemann zeta function $\zeta(s)$, it follows that $L(d_k, s) = L(\zeta^k, s) = (L(\zeta, s))^k = \zeta(s)^k$ for $\Re(s) > 1$ where the series converges.  -/)]theorem LSeries_d_eq_riemannZeta_pow (k : ℕ) {s : ℂ} (hs : 1 < s.re) :    LSeries (↗(d k)) s = riemannZeta s ^ k := by  change LSeries (↗(d k : ArithmeticFunction ℂ)) s = riemannZeta s ^ k  induction k with  | zero =>    simp only [d_zero, natCoe_one, pow_zero, one_eq_delta]    exact congr_fun LSeries_delta s  | succ j ih =>    have hζ : LSeriesSummable (↗(ζ : ArithmeticFunction ℂ)) s :=      LSeriesSummable_zeta_iff.mpr hs    rw [pow_succ, LSeries_congr (fun {n} _ => show (d (j + 1) : ArithmeticFunction ℂ) n =        ((d j : ArithmeticFunction ℂ) * ζ) n by rw [d_succ, natCoe_mul]) s,        LSeries_mul' (LSeries_d_summable j hs) hζ, ih]    congr 1    exact LSeries_zeta_eq_riemannZeta hs