OAI/GroupTheory/SimpleAmenable/Homology/ReducedTensorTwo.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ChainComplex.positiveIsCokernel line 13
  2. abbrev OAI.ReducedTensorTwo.inc line 23
  3. lemma OAI.ReducedTensorTwo.total_one_zero line 26
  4. lemma OAI.ReducedTensorTwo.d21_zero line 38
  5. lemma OAI.ReducedTensorTwo.inc_epi line 39
  6. def OAI.ReducedTensorTwo.raw line 53
  7. lemma OAI.ReducedTensorTwo.raw_epi line 55
  8. lemma OAI.ReducedTensorTwo.inc21_d line 59
  9. lemma OAI.ReducedTensorTwo.inc12_d line 68
  10. lemma OAI.ReducedTensorTwo.d_left_raw line 76
  11. lemma OAI.ReducedTensorTwo.d_right_raw line 78
  12. abbrev OAI.ReducedTensorTwo.πK line 86
  13. abbrev OAI.ReducedTensorTwo.πL line 87
  14. def OAI.ReducedTensorTwo.leftColimit line 88
  15. def OAI.ReducedTensorTwo.leftDesc line 91
  16. lemma OAI.ReducedTensorTwo.π_leftDesc line 93
  17. lemma OAI.ReducedTensorTwo.d_leftDesc line 95
  18. def OAI.ReducedTensorTwo.rightColimit line 102
  19. def OAI.ReducedTensorTwo.generator line 105
  20. lemma OAI.ReducedTensorTwo.π_generator line 107
  21. lemma OAI.ReducedTensorTwo.generator_epi line 112
  22. lemma OAI.ChainComplex.positiveπ_natural line 125
  23. lemma OAI.ModuleCat.tensor_epi line 133
  24. lemma OAI.ReducedTensorTwo.inc_natural line 144
  25. lemma OAI.ReducedTensorTwo.raw_natural line 151
  26. lemma OAI.ReducedTensorTwo.generator_natural line 155
  27. lemma OAI.ReducedTensorTwo.homology_epi line 164