OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootTranslation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The fractional root has its literal translation parameter. Its additive law and integral periods will be used to average over the prime residue field.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootElement_translation line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootElement_add line 38
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootElement_zero line 51
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootElement_neg line 58
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootElement_integral line 64