OAI/GroupTheory/SimpleAmenable/Homology/PiH1Coproduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiSSet.h1Cocone line 12
  2. lemma OAI.PiSSet.incl_proj_h1 line 14
  3. lemma OAI.PiSSet.h1_decomposition line 23
  4. def OAI.PiSSet.h1IsColimit line 39
  5. def OAI.MarkedH1.evalIso line 68
  6. def OAI.MarkedH1.points line 74
  7. def OAI.MarkedH1.primitive line 76
  8. lemma OAI.MarkedH1.hom_ext line 82
  9. def OAI.MarkedH1.descCocone line 91
  10. def OAI.MarkedH1.desc line 97
  11. lemma OAI.MarkedH1.primitive_desc line 102