OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeCosets.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete bottom-row coordinates for the cubed-prime correspondence. The first chart is represented by integral lower unipotents in level three.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeCoset line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeCoset_eq_iff line 15
  3. def OAI.CubicFirstMoment.cubicThetaPrincipalLower line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaPrincipalLower_value line 31
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeCoset_lower_eq_iff line 36
  6. def OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerChart line 47
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeLowerChart_injective line 51