OAI/RingTheory/DirectFiniteness/HoleSelection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.exists_avoiding_three line 11
2. structure OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.GoodHoles line 47
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.goodHoles_of_avoiding line 55
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.GoodHoles.mono line 118
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.exists_goodHoles line 126