OAI/GroupTheory/SimpleAmenable/Homology/E2Descend.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.E2Leading.boundary_top_cycle line 14
  2. lemma OAI.E2Leading.boundary_lead_zero line 30
  3. lemma OAI.E2Leading.boundary_lead line 52
  4. def OAI.E2Leading.descendedLead line 77
  5. lemma OAI.E2Leading.descendedLead_injective line 82
  6. lemma OAI.E2Leading.first_descendedLead_surjective line 88
  7. def OAI.TotalProjection.edgeData line 103
  8. lemma OAI.TotalProjection.edgeData_current line 117
  9. lemma OAI.TotalProjection.edgeData_previous line 118
  10. lemma OAI.E2Leading.finite_first line 126
  11. lemma OAI.TotalFiniteness.finite_first line 156