OAI/GroupTheory/SimpleAmenable/Homology/TotalFiltration.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TotalProjection.projection_eq_zero line 18
  2. lemma OAI.TotalProjection.element_ext line 27
  3. def OAI.TotalProjection.filtration line 37
  4. lemma OAI.TotalProjection.filtration_mono line 43
  5. lemma OAI.TotalProjection.filtration_zero line 47
  6. lemma OAI.TotalProjection.filtration_top line 55
  7. lemma OAI.TotalProjection.entry_zero line 61
  8. lemma OAI.TotalProjection.inclusion_mem line 67
  9. lemma OAI.TotalProjection.d_filtration line 77
  10. def OAI.TotalProjection.filteredData line 97
  11. lemma OAI.E2Leading.d_entry line 121
  12. lemma OAI.E2Leading.d_entry' line 130
  13. lemma OAI.E2Leading.zā‚‚_top_cycle line 136
  14. def OAI.E2Leading.topCycle line 153
  15. def OAI.E2Leading.row line 158
  16. lemma OAI.E2Leading.zā‚‚_top_horizontal line 161
  17. def OAI.E2Leading.topRowCycle line 183
  18. def OAI.E2Leading.lead line 187