OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalLifts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Two local lifts of the actual arithmetic quotient differ by one fixed deck transformation near any point. This is the local transition law for both the geometric charts and the cubic multiplier.

  1. lemma OAI.CubicFirstMoment.cubicThetaLocalLifts_eq line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaLocalLifts_deck line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaLocalLifts_deck_unique line 32