OAI/GroupTheory/SimpleAmenable/Configurations/SymmetricConfiguration.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.SymmetricConfiguration.G line 11
  2. def OAI.SimpleAmenable.SymmetricConfiguration.Configuration line 12
  3. instance OAI.SimpleAmenable.SymmetricConfiguration.(instance at line 14) line 14
  4. theorem OAI.SimpleAmenable.SymmetricConfiguration.ext line 15
  5. instance OAI.SimpleAmenable.SymmetricConfiguration.(instance at line 16) line 16
  6. theorem OAI.SimpleAmenable.SymmetricConfiguration.smul_apply line 20
  7. def OAI.SimpleAmenable.SymmetricConfiguration.standard line 21
  8. def OAI.SimpleAmenable.SymmetricConfiguration.standardLE line 22
  9. theorem OAI.SimpleAmenable.SymmetricConfiguration.transitive line 23
  10. lemma OAI.SimpleAmenable.SymmetricConfiguration.ne_smul line 26
  11. def OAI.SimpleAmenable.SymmetricConfiguration.configurationRepresentation line 27
  12. lemma OAI.SimpleAmenable.SymmetricConfiguration.commonNeighbor line 29
  13. lemma OAI.SimpleAmenable.SymmetricConfiguration.lowDegree_exact line 32
  14. def OAI.SimpleAmenable.SymmetricConfiguration.listEquiv line 36
  15. theorem OAI.SimpleAmenable.SymmetricConfiguration.listEquiv_apply_val line 53
  16. def OAI.SimpleAmenable.SymmetricConfiguration.chainEquiv line 56
  17. theorem OAI.SimpleAmenable.SymmetricConfiguration.chainEquiv_single_val line 60
  18. theorem OAI.SimpleAmenable.SymmetricConfiguration.chainEquiv_intertwines line 67
  19. def OAI.SimpleAmenable.SymmetricConfiguration.representationIso line 82
  20. abbrev OAI.SimpleAmenable.SymmetricConfiguration.column line 87
  21. def OAI.SimpleAmenable.SymmetricConfiguration.face line 91
  22. lemma OAI.SimpleAmenable.SymmetricConfiguration.face_apply line 95
  23. lemma OAI.SimpleAmenable.SymmetricConfiguration.face_smul line 98
  24. def OAI.SimpleAmenable.SymmetricConfiguration.faceHom line 101
  25. def OAI.SimpleAmenable.SymmetricConfiguration.boundary line 105
  26. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_chain line 110
  27. lemma OAI.SimpleAmenable.SymmetricConfiguration.boundary_sum line 116