OAI/GroupTheory/SimpleAmenable/Simplicial/FirstBarForwardLow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkedH1.lowOneHomologyIso line 12
2. lemma OAI.MarkedH1.row_one_two_finite line 23
3. lemma OAI.IntervalBar.Diagram.bar_low_finite line 39
4. lemma OAI.SimplicialDiagonal.finite_forward line 81
5. lemma OAI.IntervalBar.Diagram.bar₂_finite_forward line 107
6. lemma OAI.IntervalBar.Diagram.bar₃_finite_forward line 114
7. lemma OAI.IntervalBar.Diagram.triple_finite_of_bar line 124