OAI/GroupTheory/SimpleAmenable/Arithmetic/LatticeRiemann.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.fundamentalDomain_riemann_error line 16
  2. theorem OAI.SimpleAmenable.balanced_cutUnit_pos line 59
  3. theorem OAI.SimpleAmenable.quadraticSmallTile line 85
  4. def OAI.SimpleAmenable.pairedQuadraticBasis line 121
  5. theorem OAI.SimpleAmenable.pairedQuadraticDomain line 126
  6. theorem OAI.SimpleAmenable.pairedQuadratic_volume line 135
  7. def OAI.SimpleAmenable.pairedQuadraticEmbedding line 154
  8. theorem OAI.SimpleAmenable.pairedQuadraticEmbedding_injective line 158
  9. theorem OAI.SimpleAmenable.pairedQuadratic_span line 164
  10. def OAI.SimpleAmenable.pairedLatticeEquiv line 173
  11. theorem OAI.SimpleAmenable.pairedLatticeEquiv_coe line 180
  12. def OAI.SimpleAmenable.pairedQuadraticBox line 185
  13. theorem OAI.SimpleAmenable.pairedQuadraticBox_rectangles line 188
  14. theorem OAI.SimpleAmenable.pairedQuadraticBox_finite line 208
  15. theorem OAI.SimpleAmenable.pairedQuadraticBox_card line 216