OAI/GroupTheory/SimpleAmenable/Homology/Coefficient.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ChainComplex.zeroπ line 12
  2. instance OAI.ChainComplex.(instance at line 13) line 13
  3. lemma OAI.ChainComplex.d_zeroπ line 14
  4. def OAI.ChainComplex.zeroDesc line 15
  5. lemma OAI.ChainComplex.zeroπ_desc line 17
  6. def OAI.CoefficientNerve.point line 23
  7. def OAI.CoefficientNerve.zeroι line 24
  8. lemma OAI.CoefficientNerve.d10 line 26
  9. def OAI.CoefficientNerve.edge line 30
  10. lemma OAI.CoefficientNerve.single_d10 line 32
  11. lemma OAI.CoefficientNerve.zeroι_naturality line 52
  12. def OAI.CoefficientNerve.zeroCocone line 57
  13. lemma OAI.CoefficientNerve.desc_d10 line 61
  14. def OAI.CoefficientNerve.zeroIsColimit line 67
  15. def OAI.CoefficientNerve.zeroIso line 86