TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.odlyzkoScale : ℝ

An odlyzko scale used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.odlyzkoScale = 41 / 50

theorem NumberField.Odlyzko.odlyzkoScale_pos : 0 < odlyzkoScale

theorem NumberField.Odlyzko.degreeCorrection_le_degreeEighteen {n : ℕ} (hn : 18 ≤ n) : 12 * Real.pi / (5 * ↑n * odlyzkoScale) ≤ 20 * Real.pi / 123