OAI/NumberTheory/CubicMoment/Theta/CubicThetaQuotientCharts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Concrete local coordinate charts for the principal quotient, obtained from the proved covering map and the open positive-height half-space.

  1. def OAI.CubicFirstMoment.positiveHeightOpen line 12
  2. def OAI.CubicFirstMoment.cubicThetaPointInclusion line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPointInclusion_coe line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaPointInclusion_source line 21
  5. lemma OAI.CubicFirstMoment.cubicThetaPointInclusion_target line 23
  6. def OAI.CubicFirstMoment.cubicThetaQuotientLift line 27
  7. lemma OAI.CubicFirstMoment.cubicThetaQuotientLift_map line 30
  8. def OAI.CubicFirstMoment.cubicThetaCoveringChart line 34
  9. lemma OAI.CubicFirstMoment.cubicThetaCoveringChart_source line 38
  10. lemma OAI.CubicFirstMoment.cubicThetaCoveringChart_coe line 42
  11. def OAI.CubicFirstMoment.cubicThetaQuotientChart line 46
  12. lemma OAI.CubicFirstMoment.cubicThetaQuotientChart_source line 50
  13. instance OAI.CubicFirstMoment.cubicThetaQuotient_chartedSpace line 57