OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootSections.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-cover section space and its fractional root action.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootPoint_intertwines line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootPoint_continuous line 20
  3. def OAI.CubicFirstMoment.cubicThetaPrimeRootSections line 31
  4. def OAI.CubicFirstMoment.cubicThetaPrimeRootSectionRestrict line 46
  5. def OAI.CubicFirstMoment.cubicThetaPrimeRootSectionTranslate line 49