OAI/NumberTheory/CubicMoment/Theta/CubicThetaCubeCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Every nonzero cubic Eisenstein integer has exactly one ideal exponent vector and one of two signs. This removes the cube-root multiplicity.

  1. lemma OAI.CubicFirstMoment.eisenstein_unit_cube_sign line 12
  2. def OAI.CubicFirstMoment.cubicThetaSignedCube line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaSignedCube_ne_zero line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaSignedCube_is_cube line 28
  5. lemma OAI.CubicFirstMoment.cubicTheta_idealExponentOf_neg line 34
  6. lemma OAI.CubicFirstMoment.cubicThetaSignedCube_exponent line 38
  7. abbrev OAI.CubicFirstMoment.CubicThetaNonzeroCube line 45
  8. def OAI.CubicFirstMoment.cubicThetaCubeCoordinatesMap line 47
  9. lemma OAI.CubicFirstMoment.cubicThetaCubeCoordinates_bijective line 51
  10. def OAI.CubicFirstMoment.cubicThetaCubeCoordinates line 92
  11. lemma OAI.CubicFirstMoment.cubicThetaSignedCube_norm line 95