OAI/NumberTheory/CubicMoment/Theta/CubicThetaFreeAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The level-three quotient is a genuine covering: the actual principal congruence action has no nontrivial point stabilizers.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrincipalComplex_injective line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPrincipal_fixed_eq_one line 23
  3. instance OAI.CubicFirstMoment.cubicThetaPrincipalPointAction_free line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaQuotient_covering line 41
  5. lemma OAI.CubicFirstMoment.cubicThetaQuotient_localHomeomorph line 45