OAI/GroupTheory/SimpleAmenable/Simplicial/FinitePowerConnected.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BarFinitePower.LowConnected line 16
2. lemma OAI.BarFinitePower.LowConnected.of_iso line 19
3. lemma OAI.BarFinitePower.LowConnected.one line 21
4. lemma OAI.BarFinitePower.LowConnected.projection_isIso line 23
5. lemma OAI.BarFinitePower.LowConnected.tensor line 28
6. lemma OAI.BarFinitePower.LowConnected.fin line 34
7. lemma OAI.BarFinitePower.LowConnected.power line 38
8. lemma OAI.BarFinitePower.coordinates_fin_isIso_connected line 44
9. lemma OAI.BarFinitePower.coordinates_isIso_connected line 62