Zero Free Rectangles

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.poleClearedCompletedDedekindZetaContinuation_ne_zero_of_re_lt_zero (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {s : ℂ} (hs : s.re < 0) : poleClearedCompletedDedekindZetaContinuation K s ≠ 0