OAI/NumberTheory/CubicMoment/Estimates/RamifiedCubicValues.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Two exact cubic-symbol values detect the unit and ramified factors. Their values are computed from the finite Euler definition.

  1. lemma OAI.CubicFirstMoment.primary_neg_two line 11
  2. lemma OAI.CubicFirstMoment.normNat_neg_two line 13
  3. lemma OAI.CubicFirstMoment.cubicSymbol_neg_two_omega line 19
  4. lemma OAI.CubicFirstMoment.cubicSymbol_neg_two_lambda line 23
  5. lemma OAI.CubicFirstMoment.primary_seven_factor line 28
  6. lemma OAI.CubicFirstMoment.normNat_seven_factor line 30
  7. lemma OAI.CubicFirstMoment.primaryPrime_seven_factor line 38
  8. lemma OAI.CubicFirstMoment.cubicSymbol_seven_factor_lambda line 41
  9. lemma OAI.CubicFirstMoment.cubicSymbol_seven_factor_omega line 52