OAI/GroupTheory/SimpleAmenable/Homology/MarkedLowHomology.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MarkedH1.differential1 line 12
2. lemma OAI.MarkedH1.differential2 line 32
3. lemma OAI.MarkedH1.differential3 line 58
4. def OAI.MarkedH1.lowHomologyIso line 90
5. def OAI.CommMonoidOpposite.functor line 112
6. instance OAI.CommMonoidOpposite.(instance at line 117) line 117
7. instance OAI.CommMonoidOpposite.(instance at line 119) line 119
8. instance OAI.CommMonoidOpposite.(instance at line 121) line 121
9. instance OAI.CommMonoidOpposite.(instance at line 123) line 123
10. def OAI.CommMonoidOpposite.homologyIso line 124