OAI/NumberTheory/CubicMoment/Angular/AngularLongPrimeSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every fixed power saving for the literal free prime, with the polynomial norm-twist and excluded-prime costs already absorbed.

  1. theorem OAI.CubicFirstMoment.angular_long_prime_moebius_saving line 16