OAI/Algebra/OddKaplansky/GreedyFormula.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OddKaplansky.GreedyRing.inverse_basis line 14
2. lemma OAI.OddKaplansky.GreedyRing.imageBasis_coordinate line 18
3. lemma OAI.OddKaplansky.GreedyRing.inverse_first_projection line 35
4. lemma OAI.OddKaplansky.GreedyRing.coordinateEquiv_symm_formula line 56
5. lemma OAI.OddKaplansky.GreedyRing.rectangleY_formula line 59
6. lemma OAI.OddKaplansky.GreedyRing.coordinateEquiv_formula line 74
7. lemma OAI.OddKaplansky.GreedyRing.rectangleJ_formula line 82