OAI/NumberTheory/CubicMoment/Theta/CubicThetaQuotientManifold.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual principal quotient is a smooth real three-dimensional manifold. Chart changes are the already proved smooth arithmetic actions.

  1. lemma OAI.CubicFirstMoment.cubicThetaQuotientChart_transition_contDiff line 12
  2. instance OAI.CubicFirstMoment.cubicThetaQuotient_isManifold line 27