OAI/NumberTheory/DukePrimeDegree/Arithmetic/StarkScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The normal-closure simple-zero scale

The discriminant and zero-box bounds provide a fixed positive scale, depending only on the degree, on which a normal-closure zero is simple. This converts that statement to the integer multiplicities used by the descent argument.

  1. theorem OAI.DukePrimeDegree.zetaMultiplicity_eq_zeroMultiplicity line 22
  2. lemma OAI.DukePrimeDegree.real_mem_scaled_normalClosure_box line 31
  3. theorem OAI.DukePrimeDegree.normalClosure_simple_zero_scaled line 60