OAI/Algebra/OddKaplansky/Fourier.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.CharacterIdempotents.projector line 13
  2. lemma OAI.OddKaplansky.CharacterIdempotents.sum_character_eq_zero line 16
  3. lemma OAI.OddKaplansky.CharacterIdempotents.projector_mul_single line 31
  4. lemma OAI.OddKaplansky.CharacterIdempotents.projector_mul line 47
  5. lemma OAI.OddKaplansky.CharacterIdempotents.projector_idempotent line 61
  6. lemma OAI.OddKaplansky.CharacterIdempotents.projector_orthogonal line 67
  7. lemma OAI.OddKaplansky.CharacterIdempotents.projector_one_coeff line 80
  8. lemma OAI.OddKaplansky.CharacterIdempotents.projector_ne_zero line 84
  9. def OAI.OddKaplansky.CharacterIdempotents.pushed line 91
  10. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_eq_sum line 94
  11. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_idempotent line 99
  12. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_orthogonal line 105
  13. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_ne_zero line 110
  14. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_mul_single line 115
  15. lemma OAI.OddKaplansky.CharacterIdempotents.pushed_central line 121
  16. lemma OAI.OddKaplansky.CharacterIdempotents.lift_pushed line 137
  17. abbrev OAI.OddKaplansky.Fourier.C line 151
  18. abbrev OAI.OddKaplansky.Fourier.A line 152
  19. def OAI.OddKaplansky.Fourier.cyclicCharacter line 154
  20. lemma OAI.OddKaplansky.Fourier.cyclicCharacter_injective line 156
  21. def OAI.OddKaplansky.Fourier.character line 163
  22. lemma OAI.OddKaplansky.Fourier.character_apply line 169
  23. lemma OAI.OddKaplansky.Fourier.character_symm line 173
  24. lemma OAI.OddKaplansky.Fourier.character_mul line 176
  25. lemma OAI.OddKaplansky.Fourier.character_mulSingle line 183
  26. lemma OAI.OddKaplansky.Fourier.character_injective line 192
  27. lemma OAI.OddKaplansky.Fourier.character_one line 200
  28. lemma OAI.OddKaplansky.Fourier.character_ne_one line 204
  29. lemma OAI.OddKaplansky.Fourier.sum_inverse_characters line 208
  30. lemma OAI.OddKaplansky.Fourier.sum_projector line 220