OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical220.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7040 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw7040step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw7040step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7040 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw7041 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw7041step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw7041step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7041 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw7042 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw7042step0 line 61
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical7042 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw7043 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw7043step0 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw7043step1 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7043 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw7044 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw7044step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw7044step1 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7044 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw7045 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw7045step0 line 112
  22. def OAI.MUB6.Certificate.PairSemantics.raw7045step1 line 114
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7045 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw7046 line 129
  25. def OAI.MUB6.Certificate.PairSemantics.raw7046step0 line 131
  26. def OAI.MUB6.Certificate.PairSemantics.raw7046step1 line 133
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7046 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw7047 line 148
  29. def OAI.MUB6.Certificate.PairSemantics.raw7047step0 line 150
  30. def OAI.MUB6.Certificate.PairSemantics.raw7047step1 line 152
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7047 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw7048 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw7048step0 line 169
  34. def OAI.MUB6.Certificate.PairSemantics.raw7048step1 line 171
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7048 line 173
  36. def OAI.MUB6.Certificate.PairSemantics.raw7049 line 186
  37. def OAI.MUB6.Certificate.PairSemantics.raw7049step0 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw7049step1 line 190
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7049 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw7050 line 205
  41. def OAI.MUB6.Certificate.PairSemantics.raw7050step0 line 207
  42. def OAI.MUB6.Certificate.PairSemantics.raw7050step1 line 209
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7050 line 211
  44. def OAI.MUB6.Certificate.PairSemantics.raw7051 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw7051step0 line 226
  46. def OAI.MUB6.Certificate.PairSemantics.raw7051step1 line 228
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical7051 line 230
  48. def OAI.MUB6.Certificate.PairSemantics.raw7052 line 243
  49. def OAI.MUB6.Certificate.PairSemantics.raw7052step0 line 245
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7052 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw7053 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw7053step0 line 258
  53. def OAI.MUB6.Certificate.PairSemantics.raw7053step1 line 260
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7053 line 262
  55. def OAI.MUB6.Certificate.PairSemantics.raw7054 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw7054step0 line 277
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7054 line 279
  58. def OAI.MUB6.Certificate.PairSemantics.raw7055 line 288
  59. def OAI.MUB6.Certificate.PairSemantics.raw7055step0 line 290
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical7055 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw7056 line 301
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7056 line 303
  63. def OAI.MUB6.Certificate.PairSemantics.raw7057 line 307
  64. def OAI.MUB6.Certificate.PairSemantics.raw7057step0 line 309
  65. def OAI.MUB6.Certificate.PairSemantics.raw7057step1 line 311
  66. def OAI.MUB6.Certificate.PairSemantics.raw7057step2 line 313
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical7057 line 315
  68. def OAI.MUB6.Certificate.PairSemantics.raw7058 line 332
  69. def OAI.MUB6.Certificate.PairSemantics.raw7058step0 line 334
  70. def OAI.MUB6.Certificate.PairSemantics.raw7058step1 line 336
  71. def OAI.MUB6.Certificate.PairSemantics.raw7058step2 line 338
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7058 line 340
  73. def OAI.MUB6.Certificate.PairSemantics.raw7059 line 357
  74. def OAI.MUB6.Certificate.PairSemantics.raw7059step0 line 359
  75. def OAI.MUB6.Certificate.PairSemantics.raw7059step1 line 361
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7059 line 363
  77. def OAI.MUB6.Certificate.PairSemantics.raw7060 line 376
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7060 line 378
  79. def OAI.MUB6.Certificate.PairSemantics.raw7061 line 382
  80. def OAI.MUB6.Certificate.PairSemantics.raw7061step0 line 384
  81. def OAI.MUB6.Certificate.PairSemantics.raw7061step1 line 386
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7061 line 388
  83. def OAI.MUB6.Certificate.PairSemantics.raw7062 line 401
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7062 line 403
  85. def OAI.MUB6.Certificate.PairSemantics.raw7063 line 407
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical7063 line 409
  87. def OAI.MUB6.Certificate.PairSemantics.raw7064 line 413
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical7064 line 415
  89. def OAI.MUB6.Certificate.PairSemantics.raw7065 line 419
  90. def OAI.MUB6.Certificate.PairSemantics.raw7065step0 line 421
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7065 line 423
  92. def OAI.MUB6.Certificate.PairSemantics.raw7066 line 432
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7066 line 434
  94. def OAI.MUB6.Certificate.PairSemantics.raw7067 line 438
  95. def OAI.MUB6.Certificate.PairSemantics.raw7067step0 line 440
  96. def OAI.MUB6.Certificate.PairSemantics.raw7067step1 line 442
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7067 line 444
  98. def OAI.MUB6.Certificate.PairSemantics.raw7068 line 457
  99. def OAI.MUB6.Certificate.PairSemantics.raw7068step0 line 459
  100. def OAI.MUB6.Certificate.PairSemantics.raw7068step1 line 461
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7068 line 463
  102. def OAI.MUB6.Certificate.PairSemantics.raw7069 line 476
  103. def OAI.MUB6.Certificate.PairSemantics.raw7069step0 line 478
  104. def OAI.MUB6.Certificate.PairSemantics.raw7069step1 line 480
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7069 line 482
  106. def OAI.MUB6.Certificate.PairSemantics.raw7070 line 495
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7070 line 497
  108. def OAI.MUB6.Certificate.PairSemantics.raw7071 line 501
  109. def OAI.MUB6.Certificate.PairSemantics.raw7071step0 line 503
  110. def OAI.MUB6.Certificate.PairSemantics.raw7071step1 line 505
  111. def OAI.MUB6.Certificate.PairSemantics.raw7071step2 line 507
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7071 line 509