OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeResidueStep.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

One step in the finite three-level valuation partition used by the cubed-prime trace. Multiplication by p parametrizes the nonunits exactly.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeNonunitPart line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueStep_divisible line 14
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueStepMap line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueStepMap_injective line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueStepMap_surjective line 38
  6. def OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueStepEquiv line 53
  7. def OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueSplit line 59
  8. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueSum_split line 69
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueSum_three line 80
  10. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueSum_two line 89
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeResidueSum_one line 99