OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticCriticalImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual arithmetic residue lies in the critical local Fourier image; both required coefficient identities have been proved.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidue_critical_image line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticResidue_prime_defects_zero line 20