OAI/GroupTheory/FiniteType/FreeTensorPureMem.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FreeTensor.pure_mem line 12
  2. lemma OAI.FreeTensor.single_mem_supported line 23
  3. def OAI.ListChains.based line 37
  4. def OAI.ListChains.contraction line 46
  5. def OAI.ListChains.biDegree line 54
  6. def OAI.ListChains.biDegreeModule line 56
  7. def OAI.ListChains.biVertexModule line 59
  8. lemma OAI.ListChains.tensor_mem_degree line 62
  9. lemma OAI.ListChains.tensor_mem_vertices line 70
  10. lemma OAI.ListChains.biBoundary_lowers line 78
  11. lemma OAI.ListChains.biBoundary_vertices line 105
  12. lemma OAI.ListChains.biAugmentation_single line 121
  13. lemma OAI.ListChains.biAugmentation_biCone line 130
  14. def OAI.ListChains.biBased line 139
  15. def OAI.ListChains.biContraction line 148
  16. lemma OAI.ListChains.biVertexModule_mono line 158
  17. lemma OAI.ListChains.K_mem_vertices line 163
  18. lemma OAI.ListChains.biCone_mem_vertices line 168
  19. lemma OAI.ListChains.biCone_mem_degree line 184
  20. lemma OAI.ListChains.vertices_map line 213
  21. lemma OAI.ListChains.mapChain_mem_vertices line 225
  22. lemma OAI.ListChains.mapChain_mem_degree line 237
  23. def OAI.ListChains.diagTensor line 247
  24. lemma OAI.ListChains.biBoundary_diagTensor line 251
  25. lemma OAI.ListChains.biAugmentation_diagTensor line 255
  26. lemma OAI.ListChains.diagTensor_single_vertices line 259
  27. lemma OAI.ListChains.diagTensor_mem_degree line 273
  28. def OAI.ListChains.productComparison line 285
  29. lemma OAI.ListChains.boundary_productComparison line 289
  30. lemma OAI.ListChains.augmentation_productComparison line 293
  31. lemma OAI.ListChains.productComparison_single_vertices line 297
  32. lemma OAI.ListChains.productComparison_mem_vertices line 314
  33. lemma OAI.ListChains.productComparison_mem_degree line 322
  34. def OAI.ListChains.diagonalHomotopy line 334
  35. lemma OAI.ListChains.boundary_diagonalHomotopy line 339
  36. lemma OAI.ListChains.diagonalHomotopy_single_vertices line 352
  37. lemma OAI.ListChains.diagonalHomotopy_mem_degree line 370
  38. lemma OAI.ListChains.sign_squared line 393
  39. lemma OAI.ListChains.sign_eq_smul_of_degree line 401
  40. lemma OAI.ListChains.sign_map_of_degree line 411
  41. lemma OAI.ListChains.sign_map_of_raising line 424
  42. def OAI.ListChains.tensorHomotopy line 438
  43. lemma OAI.ListChains.tensorHomotopy_tensor line 441
  44. theorem OAI.ListChains.boundary_tensorHomotopy line 446