OAI/GroupTheory/SimpleAmenable/Homology/TotalProjection.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TotalProjection.c line 15
  2. def OAI.TotalProjection.projection line 18
  3. lemma OAI.TotalProjection.inclusion_projection line 22
  4. lemma OAI.TotalProjection.inclusion_projection_of_ne line 26
  5. abbrev OAI.TotalProjection.Index line 34
  6. abbrev OAI.TotalProjection.inclusion line 35
  7. abbrev OAI.TotalProjection.proj line 37
  8. lemma OAI.TotalProjection.sum_projection_inclusion line 39
  9. lemma OAI.TotalProjection.hom_ext line 54
  10. lemma OAI.TotalProjection.D₁_projection line 59
  11. lemma OAI.TotalProjection.D₂_projection line 81
  12. lemma OAI.TotalProjection.d_projection line 104
  13. lemma OAI.FilteredFiniteness.finite_of_ker_le line 125
  14. structure OAI.FilteredFiniteness.Data line 138
  15. def OAI.FilteredFiniteness.Data.dCycles line 150
  16. abbrev OAI.FilteredFiniteness.Data.H line 155
  17. def OAI.FilteredFiniteness.Data.π line 157
  18. def OAI.FilteredFiniteness.Data.cycles line 159
  19. def OAI.FilteredFiniteness.Data.πp line 162
  20. def OAI.FilteredFiniteness.Data.filtration line 164
  21. lemma OAI.FilteredFiniteness.Data.filtration_mono line 166
  22. def OAI.FilteredFiniteness.Data.Z₂ line 171
  23. def OAI.FilteredFiniteness.Data.B₂ line 173
  24. lemma OAI.FilteredFiniteness.Data.B₂_le_Z₂ line 176
  25. abbrev OAI.FilteredFiniteness.Data.E₂ line 187
  26. def OAI.FilteredFiniteness.Data.lead line 189
  27. lemma OAI.FilteredFiniteness.Data.lead_eq_zero line 197
  28. lemma OAI.FilteredFiniteness.Data.lower_of_lead_zero line 201
  29. lemma OAI.FilteredFiniteness.Data.finite_step line 224
  30. lemma OAI.FilteredFiniteness.Data.finite_H line 241