ArithmeticFunction.Complex.one_add_prime_cpow_ne_zero

@[blueprint  "Complex.one_add_prime_cpow_ne_zero"  (title := "Complex.one-add-prime-cpow-ne-zero")  (statement := /--    For $1<\Re(s)$ and $p$ prime, we have that $1+p^{-s}\neq 0$. The naming convention is to mimic    \begin{verbatim}      Complex.one_sub_prime_cpow_ne_zero    \end{verbatim}  -/)  (proof := /--    Suppose for contradiction $1+p^{-s}=0$, then $|p^{-s}|=1$. However, this can not happen per    \begin{verbatim}      Complex.norm_prime_cpow_le_one_half    \end{verbatim}  -/)]lemma Complex.one_add_prime_cpow_ne_zero {p : ℕ} (hp : Nat.Prime p) {s : ℂ} (hs : 1 < s.re) :    1 + (p : ℂ) ^ (-s) ≠ 0 := by  intro h  have one_add_prime_cpow_h : ‖(p : ℂ) ^ (-s)‖ = 1 := by    have := congr_arg norm (neg_eq_of_add_eq_zero_left h)    simp only [norm_neg, one_mem, CStarRing.norm_of_mem_unitary] at this    exact this  linarith [Complex.norm_prime_cpow_le_one_half ⟨p, hp⟩ hs]