OAI/NumberTheory/CubicMoment/Theta/CubicThetaChartTransition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

On every overlap, quotient coordinates differ locally by the actual smooth Mobius action of one element of the principal group.

  1. def OAI.CubicFirstMoment.cubicThetaChartTransition line 14
  2. def OAI.CubicFirstMoment.cubicThetaChartTransitionSource line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaChartTransition_deck line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaChartTransition_contDiffAt line 58