OAI/Algebra/OddKaplansky/CosetGreedy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.OrderedCosetMatrix.augmentation line 20
2. lemma OAI.OddKaplansky.OrderedCosetMatrix.augmentation_unit line 21
3. lemma OAI.OddKaplansky.OrderedCosetMatrix.representation_idempotent line 91
4. lemma OAI.OddKaplansky.OrderedCosetMatrix.greedy_pair line 140
5. def OAI.OddKaplansky.OrderedCosetMatrix.explicitJ line 148
6. def OAI.OddKaplansky.OrderedCosetMatrix.explicitY line 151
7. lemma OAI.OddKaplansky.OrderedCosetMatrix.explicit_products line 154