OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing an unramified prime cube preserves the exact arithmetic support. Consequently cube scaling holds on every index, including the zero extension of all three coefficient families.

  1. lemma OAI.CubicFirstMoment.cubicThetaCoordinates_primeCube_dvd line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaCoordinates_remove_primeCube line 26
  3. theorem OAI.CubicFirstMoment.cubicThetaCoordinates_primeCube_iff line 44
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_primeCube line 52
  5. theorem OAI.CubicFirstMoment.cubicThetaCuspCoefficient_primeCube line 61