OAI/GroupTheory/SimpleAmenable/PolygonGeometry/FlagArrangementControl.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.flagValue_arrangement line 16
  2. theorem OAI.SimpleAmenable.flagMem_arrangement line 40
  3. theorem OAI.SimpleAmenable.separatorMatrix_zero_of_cut line 48
  4. theorem OAI.SimpleAmenable.separatorMatrix_ne_zero_signs line 63
  5. theorem OAI.SimpleAmenable.separatorMatrix_controls_step line 71
  6. theorem OAI.SimpleAmenable.floor_add_unit line 90
  7. def OAI.SimpleAmenable.squareTranslationPeriod line 105
  8. theorem OAI.SimpleAmenable.squareTranslationPeriod_arrangement line 109
  9. theorem OAI.SimpleAmenable.squareTranslationPeriod_germ line 130
  10. theorem OAI.SimpleAmenable.squareTranslationPeriod_flagValue line 158
  11. theorem OAI.SimpleAmenable.squareArrangement_pair line 163
  12. theorem OAI.SimpleAmenable.squareArrangement_finite_family line 171