OAI/NumberTheory/CubicMoment/Theta/CubicThetaCommonIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual dual support is indexed once by its unit, ramified order, squarefree primary factor and primary cube factor.

  1. abbrev OAI.CubicFirstMoment.CubicThetaCommonIndex line 12
  2. def OAI.CubicFirstMoment.cubicThetaCommonNumerator line 14
  3. def OAI.CubicFirstMoment.cubicThetaCommonCoordinates line 17
  4. lemma OAI.CubicFirstMoment.cubicThetaCommonNumerator_injective line 28
  5. lemma OAI.CubicFirstMoment.cubicThetaCommonNumerator_range line 40
  6. theorem OAI.CubicFirstMoment.cubicThetaCommon_tsum line 50
  7. theorem OAI.CubicFirstMoment.cubicThetaCommon_weighted_tsum line 56