OAI/GroupTheory/SimpleAmenable/Homology/ProductNatural.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProductChains.map line 15
  2. def OAI.ProductChains.chainMap line 18
  3. def OAI.ProductChains.twoFreeMap line 20
  4. lemma OAI.ProductChains.free_natural line 25
  5. def OAI.ProductChains.tensorBiMap line 31
  6. lemma OAI.ProductChains.tensor_natural line 36
  7. def OAI.ProductChains.homologyIsoN line 49
  8. lemma OAI.ProductChains.homology_natural line 53
  9. lemma OAI.TensorCoefficient.flatPresentation line 87
  10. lemma OAI.TensorCoefficient.flat_isZero line 109
  11. lemma OAI.TensorCoefficient.arbitrary_zero_succ line 114
  12. lemma OAI.TensorCoefficient.arbitrary_zero_zero line 123
  13. lemma OAI.TensorProductHomology.arbitrary_isZero line 143
  14. instance OAI.ChainTensor.monoidalPreadditive line 161