OAI/Algebra/OddKaplansky/WreathBasis.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OddKaplansky.CharacterIdempotents.character_pairing line 13
2. def OAI.OddKaplansky.CharacterIdempotents.evaluate line 26
3. lemma OAI.OddKaplansky.CharacterIdempotents.evaluate_projector line 28
4. lemma OAI.OddKaplansky.WreathFourier.rho_projector line 45
5. def OAI.OddKaplansky.WreathFourier.normal line 74
6. lemma OAI.OddKaplansky.WreathFourier.rho_normal line 77