OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedResiduePeriodicity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact ramified cube periodicity of the actual arithmetic residue, deduced from the identified primary residue.

  1. theorem OAI.CubicFirstMoment.cubicThetaRegularizedPrimaryOne_lambda_cube line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_lambda_cube line 32
  3. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_trace_support line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_lambda_cube_pow line 49