450theorem one_sub_eulerPrimePowerComplex_ne_zero {s : ℂ} (hs : 0 < s.re) 451 (p : Nat.Primes) : 452 1 - eulerPrimePowerComplex p s ≠ 0 := by
proof body
Tactic-mode proof.
453 have hone : eulerPrimePowerComplex p s ≠ 1 := by 454 intro h 455 have hnorm : ‖eulerPrimePowerComplex p s‖ = 1 := by 456 simpa [h] 457 have hlt := norm_eulerPrimePowerComplex_lt_one hs p 458 linarith 459 exact sub_ne_zero.mpr (by simpa [eq_comm] using hone) 460 461/-- Each regularized Euler factor is nonzero on the open right half-plane. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.