OAI/GroupTheory/SimpleAmenable/Homology/RegularTotalDifferential.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RegularLabels.totalInj_d_parts line 14
  2. lemma OAI.RegularLabels.totalInj_d_hor line 21
  3. lemma OAI.RegularLabels.totalInj_d_ver line 34
  4. lemma OAI.RegularLabels.totalInj_d_both line 46
  5. lemma OAI.RegularLabels.totalInj_transport line 76
  6. lemma OAI.RegularLabels.one_totalInj line 81
  7. lemma OAI.RegularFiniteFaces.labels1_0 line 90
  8. lemma OAI.RegularFiniteFaces.weight1_0 line 93
  9. lemma OAI.RegularFiniteFaces.labels1_1 line 95
  10. lemma OAI.RegularFiniteFaces.weight1_1 line 98
  11. lemma OAI.RegularFiniteFaces.labels2_0 line 100
  12. lemma OAI.RegularFiniteFaces.weight2_0 line 104
  13. lemma OAI.RegularFiniteFaces.labels2_1 line 106
  14. lemma OAI.RegularFiniteFaces.weight2_1 line 110
  15. lemma OAI.RegularFiniteFaces.labels2_2 line 112
  16. lemma OAI.RegularFiniteFaces.weight2_2 line 116
  17. lemma OAI.RegularFiniteFaces.labels3_0 line 118
  18. lemma OAI.RegularFiniteFaces.weight3_0 line 121
  19. lemma OAI.RegularFiniteFaces.labels3_1 line 123
  20. lemma OAI.RegularFiniteFaces.weight3_1 line 126
  21. lemma OAI.RegularFiniteFaces.labels3_2 line 128
  22. lemma OAI.RegularFiniteFaces.weight3_2 line 131
  23. lemma OAI.RegularFiniteFaces.labels3_3 line 133
  24. lemma OAI.RegularFiniteFaces.weight3_3 line 136
  25. structure OAI.FilteredEdge.Data line 152
  26. def OAI.FilteredEdge.Data.current line 166
  27. def OAI.FilteredEdge.Data.previous line 168
  28. def OAI.FilteredEdge.Data.inputs line 171
  29. def OAI.FilteredEdge.Data.boundaryCycle line 172
  30. def OAI.FilteredEdge.Data.boundaryMap line 178
  31. def OAI.FilteredEdge.Data.tower line 180
  32. lemma OAI.FilteredEdge.Data.tower_mono line 182
  33. lemma OAI.FilteredEdge.Data.tower_start line 187
  34. def OAI.FilteredEdge.Data.inputLeading line 195
  35. lemma OAI.FilteredEdge.Data.lower_of_leading_zero line 200
  36. lemma OAI.FilteredEdge.Data.finite_tower_step line 218