OAI/Algebra/OddKaplansky/SectorRectangles.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.SectorOrbit.matrixPack line 16
2. lemma OAI.OddKaplansky.SectorOrbit.matrixPack_mul line 19
3. lemma OAI.OddKaplansky.SectorOrbit.matrixPack_one line 30
4. lemma OAI.OddKaplansky.SectorOrbit.pack_left_sector line 39
5. lemma OAI.OddKaplansky.SectorOrbit.rectangular line 44