OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeShiftRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The three possible rows when a prime-free frequency is multiplied by one primary prime.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeFree_primeFrequency line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeFree_unit line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_prime_zero line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_prime_one line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeFree_secondPhase line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_second_prime line 56
  7. def OAI.CubicFirstMoment.cubicThetaPrimeSecondFactor line 81
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_prime_two line 84
  9. lemma OAI.CubicFirstMoment.cubicThetaPrimePowerTerm_prime_high line 95