OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCoverGroup.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual common finite arithmetic cover on which the prime normalizer has the original cubic multiplier.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCoverGroup line 10
  2. def OAI.CubicFirstMoment.cubicThetaPrimeCoverGroupEquiv line 14
  3. instance OAI.CubicFirstMoment.cubicThetaPrimeCoverGroup_finiteIndex line 19
  4. instance OAI.CubicFirstMoment.cubicThetaPrimeCoverGroup_continuous line 26
  5. abbrev OAI.CubicFirstMoment.CubicThetaPrimeCover line 30
  6. def OAI.CubicFirstMoment.cubicThetaPrimeCoverMap line 33
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeCoverMap_open line 37
  8. instance OAI.CubicFirstMoment.cubicThetaPrimeCover_t2 line 41
  9. instance OAI.CubicFirstMoment.cubicThetaPrimeCover_locallyCompact line 44
  10. instance OAI.CubicFirstMoment.cubicThetaPrimeCover_secondCountable line 48
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeCover_covering line 52
  12. def OAI.CubicFirstMoment.cubicThetaPrimeCoverProjection line 56
  13. lemma OAI.CubicFirstMoment.cubicThetaPrimeCoverProjection_apply line 63
  14. lemma OAI.CubicFirstMoment.cubicThetaPrimeCoverProjection_continuous line 67