OAI/NumberTheory/CubicMoment/Theta/CubicThetaConstantCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The constant coefficient on cubes as the kernel size of the actual reduction of residue units to modulus three.

  1. def OAI.CubicFirstMoment.cubicThetaReductionThree line 13
  2. def OAI.CubicFirstMoment.cubicThetaUnitReductionThree line 16
  3. abbrev OAI.CubicFirstMoment.CubicThetaPrimaryResidue line 19
  4. lemma OAI.CubicFirstMoment.cubicTheta_primaryResidue_iff line 22
  5. def OAI.CubicFirstMoment.cubicThetaPrimaryResidueEquivKernel line 45
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimaryResidue_card line 64
  7. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_constant_card line 75