OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical211.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6752 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw6752step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw6752step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6752 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw6753 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw6753step0 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw6753step1 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6753 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw6754 line 52
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6754 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw6755 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw6755step0 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw6755step1 line 62
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6755 line 64
  15. def OAI.MUB6.Certificate.PairSemantics.raw6756 line 77
  16. def OAI.MUB6.Certificate.PairSemantics.raw6756step0 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw6756step1 line 81
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6756 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw6757 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw6757step0 line 98
  21. def OAI.MUB6.Certificate.PairSemantics.raw6757step1 line 100
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6757 line 102
  23. def OAI.MUB6.Certificate.PairSemantics.raw6758 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6758 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw6759 line 121
  26. def OAI.MUB6.Certificate.PairSemantics.raw6759step0 line 123
  27. def OAI.MUB6.Certificate.PairSemantics.raw6759step1 line 125
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6759 line 127
  29. def OAI.MUB6.Certificate.PairSemantics.raw6760 line 140
  30. def OAI.MUB6.Certificate.PairSemantics.raw6760step0 line 142
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6760 line 144
  32. def OAI.MUB6.Certificate.PairSemantics.raw6761 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw6761step0 line 155
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6761 line 157
  35. def OAI.MUB6.Certificate.PairSemantics.raw6762 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw6762step0 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6762 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw6763 line 179
  39. def OAI.MUB6.Certificate.PairSemantics.raw6763step0 line 181
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6763 line 183
  41. def OAI.MUB6.Certificate.PairSemantics.raw6764 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw6764step0 line 194
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6764 line 196
  44. def OAI.MUB6.Certificate.PairSemantics.raw6765 line 205
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6765 line 207
  46. def OAI.MUB6.Certificate.PairSemantics.raw6766 line 211
  47. def OAI.MUB6.Certificate.PairSemantics.raw6766step0 line 213
  48. def OAI.MUB6.Certificate.PairSemantics.raw6766step1 line 215
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6766 line 217
  50. def OAI.MUB6.Certificate.PairSemantics.raw6767 line 230
  51. def OAI.MUB6.Certificate.PairSemantics.raw6767step0 line 232
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6767 line 234
  53. def OAI.MUB6.Certificate.PairSemantics.raw6768 line 243
  54. def OAI.MUB6.Certificate.PairSemantics.raw6768step0 line 245
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6768 line 247
  56. def OAI.MUB6.Certificate.PairSemantics.raw6769 line 256
  57. def OAI.MUB6.Certificate.PairSemantics.raw6769step0 line 258
  58. def OAI.MUB6.Certificate.PairSemantics.raw6769step1 line 260
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6769 line 262
  60. def OAI.MUB6.Certificate.PairSemantics.raw6770 line 275
  61. def OAI.MUB6.Certificate.PairSemantics.raw6770step0 line 277
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6770 line 279
  63. def OAI.MUB6.Certificate.PairSemantics.raw6771 line 288
  64. def OAI.MUB6.Certificate.PairSemantics.raw6771step0 line 290
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6771 line 292
  66. def OAI.MUB6.Certificate.PairSemantics.raw6772 line 301
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6772 line 303
  68. def OAI.MUB6.Certificate.PairSemantics.raw6773 line 307
  69. def OAI.MUB6.Certificate.PairSemantics.raw6773step0 line 309
  70. def OAI.MUB6.Certificate.PairSemantics.raw6773step1 line 311
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6773 line 313
  72. def OAI.MUB6.Certificate.PairSemantics.raw6774 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw6774step0 line 328
  74. def OAI.MUB6.Certificate.PairSemantics.raw6774step1 line 330
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6774 line 332
  76. def OAI.MUB6.Certificate.PairSemantics.raw6775 line 345
  77. def OAI.MUB6.Certificate.PairSemantics.raw6775step0 line 347
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6775 line 349
  79. def OAI.MUB6.Certificate.PairSemantics.raw6776 line 358
  80. def OAI.MUB6.Certificate.PairSemantics.raw6776step0 line 360
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6776 line 362
  82. def OAI.MUB6.Certificate.PairSemantics.raw6777 line 371
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6777 line 373
  84. def OAI.MUB6.Certificate.PairSemantics.raw6778 line 377
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6778 line 379
  86. def OAI.MUB6.Certificate.PairSemantics.raw6779 line 383
  87. def OAI.MUB6.Certificate.PairSemantics.raw6779step0 line 385
  88. def OAI.MUB6.Certificate.PairSemantics.raw6779step1 line 387
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6779 line 389
  90. def OAI.MUB6.Certificate.PairSemantics.raw6780 line 402
  91. def OAI.MUB6.Certificate.PairSemantics.raw6780step0 line 404
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical6780 line 406
  93. def OAI.MUB6.Certificate.PairSemantics.raw6781 line 416
  94. def OAI.MUB6.Certificate.PairSemantics.raw6781step0 line 418
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6781 line 420
  96. def OAI.MUB6.Certificate.PairSemantics.raw6782 line 429
  97. def OAI.MUB6.Certificate.PairSemantics.raw6782step0 line 431
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical6782 line 433
  99. def OAI.MUB6.Certificate.PairSemantics.raw6783 line 442
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical6783 line 444