OAI/Algebra/OddKaplansky/WreathRepresentation.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.OddKaplansky.WreathFourier.shift_inverse_shiftline 17 - lemma
OAI.OddKaplansky.WreathFourier.shift_shift_inverseline 24 - lemma
OAI.OddKaplansky.WreathFourier.character_shift_rightline 32 - def
OAI.OddKaplansky.WreathFourier.rhoGroupline 37 - def
OAI.OddKaplansky.WreathFourier.rholine 63 - lemma
OAI.OddKaplansky.WreathFourier.rho_singleline 67 - lemma
OAI.OddKaplansky.WreathFourier.rho_topline 76