OAI/GroupTheory/SimpleAmenable/Configurations/SymmetricStable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.SymmetricConfiguration.successorStabilize line 12
2. def OAI.SimpleAmenable.SymmetricConfiguration.fullHomologySequence line 16
3. lemma OAI.SimpleAmenable.SymmetricConfiguration.successor_H1_isIso line 19
4. lemma OAI.SimpleAmenable.SymmetricConfiguration.successor_H2_isIso line 27
5. lemma OAI.SimpleAmenable.SymmetricConfiguration.fullH1_eventuallyConstant line 34
6. lemma OAI.SimpleAmenable.SymmetricConfiguration.fullH2_eventuallyConstant line 41
7. lemma OAI.SimpleAmenable.SymmetricConfiguration.fullH1_colimit_ι_isIso line 49
8. lemma OAI.SimpleAmenable.SymmetricConfiguration.fullH2_colimit_ι_isIso line 54
9. def OAI.SimpleAmenable.SymmetricConfiguration.fullH1_colimitIso line 58
10. def OAI.SimpleAmenable.SymmetricConfiguration.fullH2_colimitIso line 64
11. lemma OAI.SimpleAmenable.SymmetricConfiguration.finite_fullH1_iff_colimit line 70
12. lemma OAI.SimpleAmenable.SymmetricConfiguration.finite_fullH2_iff_colimit line 79
13. lemma OAI.SimpleAmenable.SymmetricConfiguration.stableH1_finite line 88
14. lemma OAI.SimpleAmenable.SymmetricConfiguration.stableH2_finite line 91