OAI/Algebra/OddKaplansky/GreedyRectangle.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.GreedyRing.pairing line 19
2. def OAI.OddKaplansky.GreedyRing.coordinateEquiv line 24
3. def OAI.OddKaplansky.GreedyRing.rectangleJ line 29
4. def OAI.OddKaplansky.GreedyRing.rectangleY line 31
5. lemma OAI.OddKaplansky.GreedyRing.rectangleYJ line 33
6. lemma OAI.OddKaplansky.GreedyRing.rectangleJY line 36
7. lemma OAI.OddKaplansky.GreedyRing.image_dimension line 40
8. lemma OAI.OddKaplansky.GreedyRing.pair_dimension line 43