OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeUpperChart.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The complementary chart of the cubed-prime correspondence. Its parameters are the residue classes divisible by the prime.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeWeylDenominator line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeWeylDenominator_dvd line 13
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeWeylDenominator_primary line 21
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCubeWeylRow line 26
  5. def OAI.CubicFirstMoment.cubicThetaPrimeCubeWeyl line 31
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeWeyl_c line 34
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeWeyl_d line 38
  8. def OAI.CubicFirstMoment.cubicThetaPrimeCubeUpperParameter line 42
  9. def OAI.CubicFirstMoment.cubicThetaPrimeCubeUpperRepresentative line 45
  10. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeUpperRepresentative_c line 49
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeUpperRepresentative_d line 56
  12. def OAI.CubicFirstMoment.cubicThetaPrimeCubeUpperChart line 68
  13. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeUpperChart_injective line 72