OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeResiduePeriodicity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cubic periodicity of the actual arithmetic Fourier residues follows from the saturated finite-cover averaging identity.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_cube line 13