OAI/Algebra/OddKaplansky/SectorFourier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.CharacterIdempotents.projector_pushed line 14
  2. def OAI.OddKaplansky.SectorFourier.constant line 44
  3. def OAI.OddKaplansky.SectorFourier.diagonal line 48
  4. def OAI.OddKaplansky.SectorFourier.weight line 49
  5. lemma OAI.OddKaplansky.SectorFourier.weight_shift line 50
  6. lemma OAI.OddKaplansky.SectorFourier.character_constant line 57
  7. def OAI.OddKaplansky.SectorFourier.f line 79
  8. lemma OAI.OddKaplansky.SectorFourier.f_eq_packet line 80
  9. lemma OAI.OddKaplansky.SectorFourier.diagonal_injective line 101
  10. lemma OAI.OddKaplansky.SectorFourier.diagonal_central line 110
  11. lemma OAI.OddKaplansky.SectorFourier.f_idempotent line 118
  12. lemma OAI.OddKaplansky.SectorFourier.f_ne_zero line 129
  13. lemma OAI.OddKaplansky.SectorFourier.f_central line 131