OAI/NumberTheory/CubicMoment/Estimates/CubicNumeratorOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The cubic numerator characters have odd order. In particular a nonprincipal one is not self-conjugate, as required when excluding the real-character exceptional term in the prime estimate.

  1. lemma OAI.CubicFirstMoment.cubicNumeratorLift_unit_cube line 13
  2. lemma OAI.CubicFirstMoment.cubicNumeratorChar_cube line 26
  3. lemma OAI.CubicFirstMoment.odd_cubic_character_not_self_conjugate line 36
  4. lemma OAI.CubicFirstMoment.cubicNumeratorChar_not_self_conjugate line 50
  5. lemma OAI.CubicFirstMoment.cubicNumeratorChar_ne_one_iff line 56
  6. lemma OAI.CubicFirstMoment.cubicNumeratorChar_of_cube line 80
  7. lemma OAI.CubicFirstMoment.nonprincipal_cubicNumerator_not_cube line 91