OAI/GroupTheory/SimpleAmenable/Simplicial/SimplicialAugment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimplicialAugment.aug0 line 14
2. lemma OAI.SimplicialAugment.aug0_mk line 15
3. lemma OAI.SimplicialAugment.d_aug0 line 17
4. def OAI.SimplicialAugment.aug line 27
5. lemma OAI.SimplicialAugment.aug_f_zero line 29
6. def OAI.SimplicialAugment.sec line 30
7. lemma OAI.SimplicialAugment.section_aug line 32
8. instance OAI.SimplicialAugment.flat line 40
9. lemma OAI.SimplicialAugment.lift_homology line 44
10. lemma OAI.SimplicialAugment.homology_aug line 62
11. instance OAI.SimplicialAugment.homology_aug_isIso line 79