OAI/NumberTheory/CubicMoment/Estimates/TwistedEuler.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact Euler restoration for the small-twisted primary sum. Only the primes above three and the fixed small modulus are omitted.

  1. lemma OAI.CubicFirstMoment.twisted_residue_restriction line 12
  2. theorem OAI.CubicFirstMoment.primary_smalltwist_euler line 47