OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PrivateBankWord.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.perm_list_prod_fix line 15
  2. theorem OAI.SimpleAmenable.perm_list_prod_transport line 23
  3. def OAI.SimpleAmenable.bankRow line 42
  4. def OAI.SimpleAmenable.bankColumn line 45
  5. def OAI.SimpleAmenable.bankAlphabet line 48
  6. theorem OAI.SimpleAmenable.bankRow_subset line 51
  7. theorem OAI.SimpleAmenable.bankColumn_subset line 57
  8. def OAI.SimpleAmenable.privateCycle line 63
  9. theorem OAI.SimpleAmenable.privateCycle_apply_zero line 68
  10. def OAI.SimpleAmenable.privateCycleStar line 71
  11. theorem OAI.SimpleAmenable.privateCycleStar_projection line 74
  12. theorem OAI.SimpleAmenable.bank_other_frame_notmem line 77
  13. theorem OAI.SimpleAmenable.InitialCoverSystem.private_bank_evacuation line 91