OAI/GroupTheory/SimpleAmenable/Simplicial/NerveProduct.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NerveProduct.iso line 12
  2. lemma OAI.NerveProduct.natural line 20
  3. lemma OAI.NerveProduct.fst line 22
  4. lemma OAI.NerveProduct.snd line 23
  5. def OAI.ComponentStable.reprObjectIso line 29
  6. lemma OAI.ComponentStable.tensorLeft_stable line 31
  7. lemma OAI.ComponentStable.tensorRight_stable line 48
  8. def OAI.ComponentStable.tensorFunctor line 52
  9. def OAI.ComponentStable.multiplication line 57
  10. def OAI.ComponentStable.binaryD line 59
  11. def OAI.ComponentStable.leftTensorIso line 63
  12. def OAI.ComponentStable.rightTensorIso line 69
  13. lemma OAI.ComponentStable.multiplication_left line 76
  14. lemma OAI.ComponentStable.multiplication_right line 91
  15. lemma OAI.NerveProduct.homology_congr line 116
  16. lemma OAI.ComponentStable.binaryD_left line 128
  17. lemma OAI.ComponentStable.binaryD_right line 136
  18. lemma OAI.ComponentStable.binaryD_second_left line 144
  19. lemma OAI.ComponentStable.pairLeft_multiplication line 151
  20. lemma OAI.ComponentStable.pairRight_multiplication line 160
  21. lemma OAI.ComponentStable.pairLeft_binaryD line 168
  22. lemma OAI.ComponentStable.pairRight_binaryD line 179