OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryResidue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complete primary squarefree/cube coefficient identification, up to the actual scalar base residue.

  1. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_primary_cube line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaWeightedFourierResidue_primary_cube line 27
  3. theorem OAI.CubicFirstMoment.cubicThetaWeightedFourierResidue_primary line 37
  4. theorem OAI.CubicFirstMoment.cubicThetaWeightedFourierResidue_theta_primary line 46