OAI/GroupTheory/SimpleAmenable/Simplicial/FinitePowerGeneral.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BarFinitePower.finite_tensor line 12
2. lemma OAI.BarFinitePower.finite_of_iso line 27
3. lemma OAI.BarFinitePower.finite_fin line 31
4. lemma OAI.BarFinitePower.finite_power line 47
5. def OAI.BarFinitePower.singleProject line 63
6. lemma OAI.BarFinitePower.singleProject_eval line 66
7. instance OAI.BarFinitePower.(instance at line 68) line 68
8. def OAI.BarFinitePower.doubleProject line 73
9. lemma OAI.BarFinitePower.doubleProject_eval line 77
10. instance OAI.BarFinitePower.(instance at line 79) line 79
11. def OAI.BarFinitePower.singlePowerComparison line 84
12. def OAI.BarFinitePower.doublePowerComparison line 86
13. lemma OAI.BarFinitePower.singleDegree_homology_isIso line 88
14. lemma OAI.BarFinitePower.singleRow_homology_isIso line 93
15. lemma OAI.BarFinitePower.single_power_diagonal_eq line 97
16. lemma OAI.BarFinitePower.singlePowerComparison_homology_isIso line 99
17. lemma OAI.BarFinitePower.doubleDegree_homology_isIso line 105
18. lemma OAI.BarFinitePower.doubleFirst_homology_isIso line 113
19. lemma OAI.BarFinitePower.doublePowerComparison_homology_isIso line 119
20. def OAI.IntervalBar.Diagram.outerOrder line 132
21. def OAI.IntervalBar.Diagram.outerFunctor line 134
22. instance OAI.IntervalBar.Diagram.(instance at line 136) line 136
23. instance OAI.IntervalBar.Diagram.(instance at line 138) line 138
24. instance OAI.IntervalBar.Diagram.(instance at line 145) line 145
25. instance OAI.IntervalBar.Diagram.(instance at line 166) line 166
26. instance OAI.IntervalBar.Diagram.(instance at line 217) line 217