OAI/NumberTheory/CubicMoment/Theta/CubicThetaArithmeticPrimeSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The explicit theta model has no unramified prime of valuation two. This is a property of its literal arithmetic formula, separate from the still required identification with the analytic residue.

  1. theorem OAI.CubicFirstMoment.cubicThetaCoordinates_not_square line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_prime_square line 39