OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeRootHeckeCover.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual intermediate cover from the cubic root subgroup to Iwahori(p cubed), needed to transport the cubed-prime trace pairing.

  1. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeIwahori_continuous line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRoot_le_hecke line 16
  3. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeSubgroup line 21
  4. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeSubgroup_finiteIndex line 25
  5. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeSubgroupEquiv line 30
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHecke_index line 38
  7. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeTransversal line 44
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeTransversal_complement line 48
  9. instance OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeTransversal_finite line 52
  10. def OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeDomain line 58
  11. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeDomain_measurable line 62
  12. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeDomain_unique line 69
  13. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeDomain_isFundamentalDomain line 101
  14. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeRootHeckeDomain_root_fundamental line 107