OAI/Algebra/OddKaplansky/FreeBlocks.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.WreathFourier.freeUnit line 20
2. lemma OAI.OddKaplansky.WreathFourier.freeUnit_mul line 23
3. lemma OAI.OddKaplansky.WreathFourier.freeUnit_independent line 114
4. lemma OAI.OddKaplansky.WreathFourier.topElt_normal line 198
5. lemma OAI.OddKaplansky.WreathFourier.topElt_freeUnit line 203
6. lemma OAI.OddKaplansky.WreathFourier.freeUnit_topElt line 219
7. def OAI.OddKaplansky.WreathFourier.baseElt line 235
8. lemma OAI.OddKaplansky.WreathFourier.projector_baseElt line 237
9. lemma OAI.OddKaplansky.WreathFourier.baseElt_projector line 241
10. lemma OAI.OddKaplansky.WreathFourier.topElt_baseElt line 249
11. lemma OAI.OddKaplansky.WreathFourier.baseElt_freeUnit line 256
12. lemma OAI.OddKaplansky.WreathFourier.freeUnit_baseElt line 273