OAI/GroupTheory/SimpleAmenable/Homology/CoefficientContraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SemiExtra.Data line 9
  2. def OAI.SemiExtra.homotopyEquiv line 19
  3. lemma OAI.CoefficientNerve.weighted_eq line 47
  4. def OAI.CoefficientNerve.augmentation line 54
  5. def OAI.CoefficientNerve.augmented line 62
  6. def OAI.CoefficientNerve.extra line 64
  7. lemma OAI.CoefficientNerve.single_extra line 66
  8. lemma OAI.CoefficientNerve.extra_zero line 68
  9. lemma OAI.CoefficientNerve.extra_tail_map line 74
  10. lemma OAI.CoefficientNerve.extra_succ line 82
  11. def OAI.CoefficientNerve.contraction line 94
  12. def OAI.CoefficientNerve.terminalHomotopyEquiv line 112