OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimaryCubes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The primary cubes at the inverted cusp are in exact bijection with ideals prime to lambda. No choice of a cube root contributes multiplicity.

  1. abbrev OAI.CubicFirstMoment.CubicThetaUnramifiedIdeal line 12
  2. abbrev OAI.CubicFirstMoment.CubicThetaPrimaryCube line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimaryGenerator_primary line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimaryGenerator_cube_primary line 31
  5. def OAI.CubicFirstMoment.cubicThetaPrimaryCubeMap line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimaryCubeMap_exponent line 40
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimaryCubeMap_bijective line 45
  8. def OAI.CubicFirstMoment.cubicThetaPrimaryCubeEquiv line 78
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimaryCube_norm line 81
  10. lemma OAI.CubicFirstMoment.cubicThetaPrimaryCube_units line 88