OAI/GroupTheory/SimpleAmenable/Simplicial/FirstBarDegreeTwoFinite.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntervalBar.Diagram.row_one_three_finite line 13
  2. lemma OAI.IntervalBar.Diagram.first_row_two_finite line 25
  3. def OAI.StableBarOne.insert line 50
  4. lemma OAI.StableBarOne.binary_insert_face line 53
  5. lemma OAI.StableBarOne.binary_insert_zero line 63
  6. lemma OAI.StableBarOne.binary_insert_last line 71
  7. lemma OAI.StableBarOne.binary_insert_zero_other line 79
  8. lemma OAI.StableBarOne.binary_insert_last_other line 89
  9. lemma OAI.StableBarOne.binary_insert_middle line 99
  10. lemma OAI.StableBarOne.row_d10 line 113
  11. def OAI.StableBarOne.π line 116
  12. lemma OAI.StableBarOne.d_π line 118
  13. def OAI.StableBarOne.oneIso line 120
  14. def OAI.StableBarOne.linearπ line 123
  15. instance OAI.StableBarOne.linearπ_epi line 125
  16. lemma OAI.StableBarOne.oneIso_linearπ line 128
  17. lemma OAI.StableBarOne.boundary_linearπ line 132
  18. lemma OAI.StableBarOne.eq_of_boundary line 146
  19. lemma OAI.StableBarOne.binary_linearπ line 151
  20. lemma OAI.StableBarOne.translate_linearπ line 161
  21. def OAI.StableBarOne.cocone line 166
  22. def OAI.StableBarOne.fromStable line 174
  23. lemma OAI.StableBarOne.toStable_fromStable line 176
  24. instance OAI.StableBarOne.fromStable_epi line 183
  25. lemma OAI.StableBarOne.row_one_finite line 186