OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootSections.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.cubicThetaPrimeCubeRootSections line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootPoint_intertwines line 12
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootPoint_continuous line 21
  4. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSectionTranslate line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSectionTranslate_add line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSectionTranslate_zero line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootSectionTranslate_integral line 60
  8. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootOperator line 69
  9. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootOperator_congr line 82