OAI/NumberTheory/CubicMoment/Estimates/MixedTwistedEuler.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact ramified Euler restoration for the norm-twisted primary mixed sum. These are the sums to which the smooth primitive bound is applied.

  1. theorem OAI.CubicFirstMoment.primary_mixed_twisted_euler line 13