OAI/GroupTheory/SimpleAmenable/Homology/MarkedPrimitiveFaces.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkedH1.T line 15
  2. def OAI.MarkedH1.R line 16
  3. def OAI.MarkedH1.P10 line 18
  4. def OAI.MarkedH1.P20 line 19
  5. def OAI.MarkedH1.P21 line 20
  6. def OAI.MarkedH1.P30 line 21
  7. def OAI.MarkedH1.P31 line 22
  8. def OAI.MarkedH1.P32 line 23
  9. def OAI.MarkedH1.P40 line 24
  10. def OAI.MarkedH1.P41 line 25
  11. def OAI.MarkedH1.P42 line 26
  12. def OAI.MarkedH1.P43 line 27
  13. lemma OAI.MarkedH1.Pface_2_0_0 line 28
  14. lemma OAI.MarkedH1.Pface_2_0_1 line 31
  15. lemma OAI.MarkedH1.Pface_2_0_2 line 34
  16. lemma OAI.MarkedH1.Pface_2_1_0 line 37
  17. lemma OAI.MarkedH1.Pface_2_1_1 line 40
  18. lemma OAI.MarkedH1.Pface_2_1_2 line 43
  19. lemma OAI.MarkedH1.Pface_3_0_0 line 46
  20. lemma OAI.MarkedH1.Pface_3_0_1 line 49
  21. lemma OAI.MarkedH1.Pface_3_0_2 line 52
  22. lemma OAI.MarkedH1.Pface_3_0_3 line 55
  23. lemma OAI.MarkedH1.Pface_3_1_0 line 58
  24. lemma OAI.MarkedH1.Pface_3_1_1 line 61
  25. lemma OAI.MarkedH1.Pface_3_1_2 line 64
  26. lemma OAI.MarkedH1.Pface_3_1_3 line 67
  27. lemma OAI.MarkedH1.Pface_3_2_0 line 70
  28. lemma OAI.MarkedH1.Pface_3_2_1 line 73
  29. lemma OAI.MarkedH1.Pface_3_2_2 line 76
  30. lemma OAI.MarkedH1.Pface_3_2_3 line 79
  31. lemma OAI.MarkedH1.Pface_4_0_0 line 82
  32. lemma OAI.MarkedH1.Pface_4_0_1 line 85
  33. lemma OAI.MarkedH1.Pface_4_0_2 line 88
  34. lemma OAI.MarkedH1.Pface_4_0_3 line 91
  35. lemma OAI.MarkedH1.Pface_4_0_4 line 94
  36. lemma OAI.MarkedH1.Pface_4_1_0 line 97
  37. lemma OAI.MarkedH1.Pface_4_1_1 line 100
  38. lemma OAI.MarkedH1.Pface_4_1_2 line 103
  39. lemma OAI.MarkedH1.Pface_4_1_3 line 106
  40. lemma OAI.MarkedH1.Pface_4_1_4 line 109
  41. lemma OAI.MarkedH1.Pface_4_2_0 line 112
  42. lemma OAI.MarkedH1.Pface_4_2_1 line 115
  43. lemma OAI.MarkedH1.Pface_4_2_2 line 118
  44. lemma OAI.MarkedH1.Pface_4_2_3 line 121
  45. lemma OAI.MarkedH1.Pface_4_2_4 line 124
  46. lemma OAI.MarkedH1.Pface_4_3_0 line 127
  47. lemma OAI.MarkedH1.Pface_4_3_1 line 130
  48. lemma OAI.MarkedH1.Pface_4_3_2 line 133
  49. lemma OAI.MarkedH1.Pface_4_3_3 line 136
  50. lemma OAI.MarkedH1.Pface_4_3_4 line 139
  51. lemma OAI.MarkedH1.Pd_2_0 line 152
  52. lemma OAI.MarkedH1.Pd_2_1 line 161
  53. lemma OAI.MarkedH1.Pd_3_0 line 170
  54. lemma OAI.MarkedH1.Pd_3_1 line 179
  55. lemma OAI.MarkedH1.Pd_3_2 line 188
  56. lemma OAI.MarkedH1.Pd_4_0 line 197
  57. lemma OAI.MarkedH1.Pd_4_1 line 206
  58. lemma OAI.MarkedH1.Pd_4_2 line 215
  59. lemma OAI.MarkedH1.Pd_4_3 line 224