OAI/GroupTheory/SimpleAmenable/Homology/ReducedNatural.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ConstantSplit.aug_natural line 14
  2. def OAI.ConstantSplit.redMap line 17
  3. lemma OAI.ConstantSplit.redMap_inclusion line 19
  4. lemma OAI.ConstantSplit.one_positive line 21
  5. def OAI.ConstantSplit.inclusionIso line 24
  6. lemma OAI.ConstantSplit.redMap_epi line 35
  7. lemma OAI.ConstantSplit.red_X_zero line 46
  8. def OAI.ConnectedProduct.redInclusion line 77
  9. lemma OAI.ConnectedProduct.redInclusion_redProjection line 80
  10. lemma OAI.ConnectedProduct.redInclusion_fst line 86
  11. lemma OAI.ConnectedProduct.redInclusion_snd line 108
  12. lemma OAI.ConnectedProduct.redInclusion_projection line 130
  13. lemma OAI.ConnectedProduct.red_projection_recover line 133
  14. lemma OAI.ConnectedProduct.redInclusion_natural line 146
  15. lemma OAI.ConnectedProduct.kernel_map_surjective line 154