OAI/Algebra/OddKaplansky/WreathLinear.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OddKaplansky.WreathFourier.normal_coordinate line 19
2. lemma OAI.OddKaplansky.WreathFourier.normal_independent line 33
3. instance OAI.OddKaplansky.WreathFourier.(instance at line 44) line 44
4. lemma OAI.OddKaplansky.WreathFourier.normal_card line 46
5. def OAI.OddKaplansky.WreathFourier.normalBasis line 62
6. lemma OAI.OddKaplansky.WreathFourier.normalBasis_apply line 65