exact fun h ↦ (NeZero.of_pos σpos).ne <| zero_eq_neg.mp <| zero_re ▸ h ▸ (by simp [s])
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ -s ≠ 0
no goals