OAI/Algebra/OddKaplansky/WreathFourier.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_conjugate line 15
  2. abbrev OAI.OddKaplansky.WreathFourier.Base line 36
  3. abbrev OAI.OddKaplansky.WreathFourier.Wreath line 37
  4. def OAI.OddKaplansky.WreathFourier.shift line 39
  5. lemma OAI.OddKaplansky.WreathFourier.shift_apply line 45
  6. lemma OAI.OddKaplansky.WreathFourier.shift_one line 51
  7. lemma OAI.OddKaplansky.WreathFourier.shift_mul line 57
  8. lemma OAI.OddKaplansky.WreathFourier.character_shift line 65
  9. def OAI.OddKaplansky.WreathFourier.base line 71
  10. lemma OAI.OddKaplansky.WreathFourier.base_left line 75
  11. lemma OAI.OddKaplansky.WreathFourier.base_right line 81
  12. def OAI.OddKaplansky.WreathFourier.top line 87
  13. lemma OAI.OddKaplansky.WreathFourier.base_injective line 88
  14. lemma OAI.OddKaplansky.WreathFourier.top_injective line 94
  15. lemma OAI.OddKaplansky.WreathFourier.top_conjugate line 100
  16. lemma OAI.OddKaplansky.WreathFourier.normal_form line 108
  17. def OAI.OddKaplansky.WreathFourier.projector line 115
  18. def OAI.OddKaplansky.WreathFourier.topElt line 117
  19. lemma OAI.OddKaplansky.WreathFourier.projector_idempotent line 118
  20. lemma OAI.OddKaplansky.WreathFourier.projector_orthogonal line 121
  21. lemma OAI.OddKaplansky.WreathFourier.projector_ne_zero line 124
  22. lemma OAI.OddKaplansky.WreathFourier.translated line 126
  23. lemma OAI.OddKaplansky.WreathFourier.sum_projector line 131