OAI/Algebra/OddKaplansky/HeisenbergRepresentation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.Heisenberg.character_dot line 12
  2. def OAI.OddKaplansky.Heisenberg.ρGroup line 15
  3. def OAI.OddKaplansky.Heisenberg.ρ line 32
  4. lemma OAI.OddKaplansky.Heisenberg.ρ_single line 33
  5. def OAI.OddKaplansky.Heisenberg.f line 39
  6. lemma OAI.OddKaplansky.Heisenberg.f_idempotent line 40
  7. lemma OAI.OddKaplansky.Heisenberg.f_ne_zero line 41
  8. lemma OAI.OddKaplansky.Heisenberg.f_central line 42
  9. lemma OAI.OddKaplansky.Heisenberg.ρ_f line 43
  10. def OAI.OddKaplansky.Heisenberg.p line 52
  11. def OAI.OddKaplansky.Heisenberg.D line 53
  12. lemma OAI.OddKaplansky.Heisenberg.ρ_p line 54
  13. lemma OAI.OddKaplansky.Heisenberg.ρ_D line 80
  14. def OAI.OddKaplansky.Heisenberg.xElt line 82
  15. def OAI.OddKaplansky.Heisenberg.Ω line 83
  16. lemma OAI.OddKaplansky.Heisenberg.ρ_Ω line 84