OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical318.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw10176 line 9
  2. def OAI.MUB6.Certificate.PairSemantics.raw10176step0 line 11
  3. def OAI.MUB6.Certificate.PairSemantics.raw10176step1 line 13
  4. def OAI.MUB6.Certificate.PairSemantics.raw10176step2 line 15
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical10176 line 17
  6. def OAI.MUB6.Certificate.PairSemantics.raw10177 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw10177step0 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw10177step1 line 38
  9. def OAI.MUB6.Certificate.PairSemantics.raw10177step2 line 40
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical10177 line 42
  11. def OAI.MUB6.Certificate.PairSemantics.raw10178 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw10178step0 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw10178step1 line 63
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical10178 line 65
  15. def OAI.MUB6.Certificate.PairSemantics.raw10179 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw10179step0 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw10179step1 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical10179 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw10180 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw10180step0 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw10180step1 line 101
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical10180 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw10181 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw10181step0 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw10181step1 line 120
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical10181 line 122
  27. def OAI.MUB6.Certificate.PairSemantics.raw10182 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw10182step0 line 137
  29. def OAI.MUB6.Certificate.PairSemantics.raw10182step1 line 139
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical10182 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw10183 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw10183step0 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw10183step1 line 158
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical10183 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw10184 line 173
  36. def OAI.MUB6.Certificate.PairSemantics.raw10184step0 line 175
  37. def OAI.MUB6.Certificate.PairSemantics.raw10184step1 line 177
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical10184 line 179