OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact six-unit multiplicity in the squared theta coefficients. The order congruent to one has precisely the two real units.

  1. instance OAI.CubicFirstMoment.(instance at line 12) line 12
  2. instance OAI.CubicFirstMoment.(instance at line 14) line 14
  3. def OAI.CubicFirstMoment.cubicThetaRamifiedMass line 16
  4. lemma OAI.CubicFirstMoment.cubicTheta_real_unit_sum line 21
  5. lemma OAI.CubicFirstMoment.cubicThetaRamifiedMass_unit_sum line 41