OAI/Algebra/OddKaplansky/ModularGeneric.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.WreathFourier.shiftAction line 18
  2. def OAI.OddKaplansky.WreathFourier.lamp line 23
  3. lemma OAI.OddKaplansky.WreathFourier.weight_diagonal line 24
  4. def OAI.OddKaplansky.WreathFourier.Blocks.weights line 43
  5. def OAI.OddKaplansky.WreathFourier.Blocks.projection line 44
  6. def OAI.OddKaplansky.WreathFourier.Blocks.element line 45
  7. lemma OAI.OddKaplansky.WreathFourier.Blocks.idempotent line 46
  8. lemma OAI.OddKaplansky.WreathFourier.Blocks.annihilate line 70
  9. lemma OAI.OddKaplansky.WreathFourier.Blocks.rank_bound line 88
  10. lemma OAI.OddKaplansky.WreathFourier.modular_idempotent line 124