OAI/NumberTheory/CubicMoment/Theta/CubicThetaConstantDirichlet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact reindexing of the Eisenstein constant coefficient Dirichlet series by the two signed cubes of each nonzero ideal.

  1. def OAI.CubicFirstMoment.cubicThetaConstantTermWeight line 13
  2. def OAI.CubicFirstMoment.cubicThetaConstantDirichlet line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaConstantTermWeight_support line 20
  4. lemma OAI.CubicFirstMoment.cubicThetaConstantTermWeight_cube line 31
  5. lemma OAI.CubicFirstMoment.cubicThetaConstantDirichlet_cube_sum line 56
  6. lemma OAI.CubicFirstMoment.cubicTheta_signed_sum line 67
  7. theorem OAI.CubicFirstMoment.cubicThetaConstantDirichlet_eq_ramified line 77