OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedLowRow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Only the middle of the three retained low rows can contribute to the cubic step. Its coefficient is still the actual finite Gauss sum.

  1. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_ramified_two_row line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaRamifiedLowDirichlet_middle line 35