OAI/GroupTheory/SimpleAmenable/Homology/ConstantSplit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProductChains.chainMap_id line 17
  2. lemma OAI.ProductChains.chainMap_comp line 19
  3. lemma OAI.ProductChains.chainMap_aug line 21
  4. abbrev OAI.ConstantSplit.one line 32
  5. def OAI.ConstantSplit.aug line 33
  6. def OAI.ConstantSplit.sec line 34
  7. lemma OAI.ConstantSplit.section_aug line 35
  8. def OAI.ConstantSplit.sc line 39
  9. def OAI.ConstantSplit.splitting line 41
  10. instance OAI.ConstantSplit.aug_iso line 45
  11. lemma OAI.ConstantSplit.red_zero line 59
  12. instance OAI.ConstantSplit.red_flat line 75
  13. lemma OAI.ConnectedProduct.projection_kernel_aux line 91
  14. lemma OAI.ConnectedProduct.projection_isIso_arbitrary line 135