OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedPhaseTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The modulus-nine phase aligns the two surviving middle-row terms on each of the three positive unit representatives.

  1. theorem OAI.CubicFirstMoment.cubicThetaNinePhase_middle_first line 10
  2. theorem OAI.CubicFirstMoment.cubicThetaNinePhase_middle_second line 27