OAI/NumberTheory/CubicMoment/Angular/AngularTwistedEuler.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, with the angular character and its unit compatibility retained exactly.

  1. lemma OAI.CubicFirstMoment.angular_twisted_residue_restriction line 13
  2. theorem OAI.CubicFirstMoment.primary_angular_smalltwist_euler line 50