OAI/GroupTheory/FiniteType/FreeTensor.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeTensor.Chains line 10
  2. def OAI.FreeTensor.pure line 12
  3. lemma OAI.FreeTensor.pure_single_single line 16
  4. lemma OAI.FreeTensor.pure_single_one line 20
  5. lemma OAI.FreeTensor.ext line 26
  6. def OAI.FreeTensor.map line 37
  7. lemma OAI.FreeTensor.map_pure line 42
  8. def OAI.FreeTensor.lift line 59
  9. lemma OAI.FreeTensor.lift_pure line 63
  10. abbrev OAI.ListChains.BiChain line 85
  11. abbrev OAI.ListChains.tensor line 87
  12. abbrev OAI.ListChains.tensorMap line 90
  13. lemma OAI.ListChains.tensorMap_tensor line 94
  14. def OAI.ListChains.biBoundary line 99
  15. lemma OAI.ListChains.biBoundary_tensor line 102
  16. lemma OAI.ListChains.biBoundary_squared line 107
  17. def OAI.ListChains.biAugmentation line 117
  18. lemma OAI.ListChains.biAugmentation_tensor line 121
  19. lemma OAI.ListChains.biAugmentation_boundary line 126
  20. def OAI.ListChains.biCone line 134
  21. lemma OAI.ListChains.biCone_tensor line 137
  22. lemma OAI.ListChains.biBoundary_biCone line 142
  23. def OAI.ListChains.vertices line 162
  24. lemma OAI.ListChains.mem_vertices line 164
  25. lemma OAI.ListChains.head_mem_vertices line 167
  26. lemma OAI.ListChains.vertices_vertex line 169
  27. lemma OAI.ListChains.vertices_cone line 173
  28. lemma OAI.ListChains.degree_cone line 178
  29. lemma OAI.ListChains.supported_cone line 181
  30. theorem OAI.ListChains.boundary_faces line 189
  31. lemma OAI.ListChains.boundary_lowers line 231
  32. lemma OAI.ListChains.boundary_vertices line 235
  33. def OAI.ListChains.vertexModule line 239
  34. lemma OAI.ListChains.mem_vertexModule line 242
  35. lemma OAI.ListChains.vertex_mem_vertexModule line 246
  36. lemma OAI.ListChains.cone_mem_vertexModule line 253
  37. lemma OAI.ListChains.boundary_mem_vertexModule line 262
  38. lemma OAI.ListChains.vertexModule_mono line 270
  39. def OAI.ListChains.degreeModule line 275
  40. lemma OAI.ListChains.mem_degreeModule line 278
  41. lemma OAI.ListChains.cone_mem_degreeModule line 281
  42. lemma OAI.ListChains.vertex_mem_degreeModule line 287
  43. lemma OAI.ListChains.boundary_mem_degreeModule line 290