OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeDoubleRootSections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual sections and their fractional translations at the cube modulus.

  1. abbrev OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSections line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootPoint_intertwines line 12
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootPoint_continuous line 21
  4. def OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSectionTranslate line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSectionTranslate_add line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSectionTranslate_zero line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootSectionTranslate_integral line 60
  8. def OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootOperator line 69
  9. theorem OAI.CubicFirstMoment.cubicThetaPrimeDoubleRootOperator_congr line 82