OAI/Algebra/OddKaplansky/Heisenberg.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Heisenberg.Z line 10
  2. def OAI.OddKaplansky.Heisenberg.dot line 11
  3. lemma OAI.OddKaplansky.Heisenberg.dot_one_left line 12
  4. lemma OAI.OddKaplansky.Heisenberg.dot_one_right line 13
  5. lemma OAI.OddKaplansky.Heisenberg.dot_mul_left line 14
  6. lemma OAI.OddKaplansky.Heisenberg.dot_mul_right line 17
  7. lemma OAI.OddKaplansky.Heisenberg.dot_inv_left line 20
  8. lemma OAI.OddKaplansky.Heisenberg.dot_inv_right line 23
  9. lemma OAI.OddKaplansky.Heisenberg.dot_symm line 26
  10. structure OAI.OddKaplansky.Heisenberg.GroupData line 27
  11. lemma OAI.OddKaplansky.Heisenberg.GroupData.ext line 31
  12. instance OAI.OddKaplansky.Heisenberg.(instance at line 33) line 33
  13. instance OAI.OddKaplansky.Heisenberg.(instance at line 34) line 34
  14. instance OAI.OddKaplansky.Heisenberg.(instance at line 35) line 35
  15. lemma OAI.OddKaplansky.Heisenberg.one_x line 36
  16. lemma OAI.OddKaplansky.Heisenberg.one_y line 37
  17. lemma OAI.OddKaplansky.Heisenberg.one_k line 38
  18. lemma OAI.OddKaplansky.Heisenberg.mul_x line 39
  19. lemma OAI.OddKaplansky.Heisenberg.mul_y line 40
  20. lemma OAI.OddKaplansky.Heisenberg.mul_k line 41
  21. lemma OAI.OddKaplansky.Heisenberg.inv_x line 42
  22. lemma OAI.OddKaplansky.Heisenberg.inv_y line 43
  23. lemma OAI.OddKaplansky.Heisenberg.inv_k line 44
  24. instance OAI.OddKaplansky.Heisenberg.(instance at line 45) line 45
  25. def OAI.OddKaplansky.Heisenberg.coordinates line 50
  26. instance OAI.OddKaplansky.Heisenberg.(instance at line 55) line 55
  27. lemma OAI.OddKaplansky.Heisenberg.card line 56
  28. def OAI.OddKaplansky.Heisenberg.central line 60
  29. def OAI.OddKaplansky.Heisenberg.X line 64
  30. def OAI.OddKaplansky.Heisenberg.Y line 68
  31. lemma OAI.OddKaplansky.Heisenberg.central_injective line 72
  32. lemma OAI.OddKaplansky.Heisenberg.central_commute line 73
  33. lemma OAI.OddKaplansky.Heisenberg.YX line 76
  34. lemma OAI.OddKaplansky.Heisenberg.normal line 78