OAI/GroupTheory/SimpleAmenable/Simplicial/PowerDiagonal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BarFinitePower.liftRows line 16
2. lemma OAI.BarFinitePower.liftDiagonal line 22
3. lemma OAI.BarFinitePower.homologyLiftDiagonal_isIso line 24
4. def OAI.BarFinitePower.triplePowerComparison line 40
5. lemma OAI.BarFinitePower.tripleDegree_homology_isIso line 42
6. lemma OAI.BarFinitePower.tripleBarOne_homology_isIso line 50
7. lemma OAI.BarFinitePower.tripleBarTwo_homology_isIso line 58
8. lemma OAI.BarFinitePower.triplePowerComparison_homology_isIso line 65
9. def OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.finiteProductComparison line 75
10. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.finiteProductComparison_homology_isIso line 78