OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramRowPeriodicity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The off-diagonal row phase descends to the actual level-three translation classes of primitive rows.

  1. lemma OAI.CubicFirstMoment.cubicThetaCompletion_top_character line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRow_right_translation_c line 34
  3. lemma OAI.CubicFirstMoment.cubicThetaRow_right_translation_d line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaGramRowPhase_translation line 46