OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalLattice.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite residue coordinates for the sublattice used by a horizontal Hecke dilation.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontalLattice_bijective line 12
  2. def OAI.CubicFirstMoment.cubicThetaHorizontalLatticeEquiv line 36
  3. def OAI.CubicFirstMoment.CubicThetaScaledPeriodGroup line 40
  4. instance OAI.CubicFirstMoment.(instance at line 41) line 41
  5. instance OAI.CubicFirstMoment.(instance at line 43) line 43
  6. instance OAI.CubicFirstMoment.cubicThetaScaledPeriodGroup_action line 47
  7. instance OAI.CubicFirstMoment.cubicThetaScaledPeriodGroup_continuous line 58
  8. instance OAI.CubicFirstMoment.cubicThetaScaledPeriodGroup_measure line 64
  9. def OAI.CubicFirstMoment.cubicThetaHorizontalScaledCell line 70
  10. lemma OAI.CubicFirstMoment.cubicThetaHorizontalScaledCell_fundamental line 73