OAI/RingTheory/DirectFiniteness/SlabKeys.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabMap line 17
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabMap_injective line 23
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabMap_range_le line 29
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabMap_axis line 34
5. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabKey line 39
6. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabKey.points line 42
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabKey.nonempty line 44
8. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabKeyOf line 46
9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.mem_slabKeyOf line 51
10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabKey.unique line 53
11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabKeyOf_eq_of_mem line 63
12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.slabKeyOf_stable line 66
13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabKey.diff line 69
14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.SlabKey.holes_unique line 73