OAI/GroupTheory/SimpleAmenable/Homology/PowerEquivalence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.StageProductColimit.(instance at line 11) line 11
2. instance OAI.StageProductColimit.(instance at line 13) line 13
3. instance OAI.StageProductColimit.(instance at line 19) line 19
4. def OAI.StageProductColimit.uncurry line 21
5. def OAI.StageProductColimit.curry line 24
6. def OAI.StageProductColimit.curryEquiv line 27
7. instance OAI.StageProductColimit.(instance at line 45) line 45
8. def OAI.IntervalBar.Diagram.eval₂ line 52
9. def OAI.IntervalBar.Diagram.eval₃ line 54
10. instance OAI.IntervalBar.Diagram.(instance at line 57) line 57
11. instance OAI.IntervalBar.Diagram.(instance at line 59) line 59
12. lemma OAI.IntervalBar.Diagram.eval₂_natural line 61
13. lemma OAI.IntervalBar.Diagram.eval₃_natural line 64
14. def OAI.ColimitTransfer.ofIsos line 76
15. abbrev OAI.ColimitTransfer.H line 85
16. def OAI.ColimitTransfer.ofEquivalences line 87