OAI/RingTheory/DirectFiniteness/CandidateGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.cyclic_two_apart line 13
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.vector_mem_U line 21
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.vector_not_mem_U line 27
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.two_generic_bundle line 41
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.distinct_generic_cosets line 71
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.closed_of_points line 95