OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedRowValue.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The computed modulus-nine sum in the normalization of the actual Eisenstein rows. The sign comes from lambda squared being minus three.

  1. theorem OAI.CubicFirstMoment.cubicThetaRamifiedBaseRow_one line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_ramified_value line 71