OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical97.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3104 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw3104step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw3104step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3104 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw3105 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw3105step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw3105step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3105 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw3106 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw3106step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw3106step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3106 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw3107 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw3107step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw3107step1 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3107 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw3108 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw3108step0 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw3108step1 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3108 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw3109 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw3109step0 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw3109step1 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3109 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw3110 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw3110step0 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw3110step1 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3110 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw3111 line 152
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3111 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw3112 line 158
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3112 line 160
  33. def OAI.MUB6.Certificate.PairSemantics.raw3113 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw3113step0 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw3113step1 line 168
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3113 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw3114 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw3114step0 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw3114step1 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3114 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw3115 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw3115step0 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw3115step1 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw3115step2 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw3115step3 line 210
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3115 line 212
  47. def OAI.MUB6.Certificate.PairSemantics.raw3116 line 234
  48. def OAI.MUB6.Certificate.PairSemantics.raw3116step0 line 236
  49. def OAI.MUB6.Certificate.PairSemantics.raw3116step1 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw3116step2 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw3116step3 line 242
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3116 line 244
  53. def OAI.MUB6.Certificate.PairSemantics.raw3117 line 266
  54. def OAI.MUB6.Certificate.PairSemantics.raw3117step0 line 268
  55. def OAI.MUB6.Certificate.PairSemantics.raw3117step1 line 270
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3117 line 272
  57. def OAI.MUB6.Certificate.PairSemantics.raw3118 line 285
  58. def OAI.MUB6.Certificate.PairSemantics.raw3118step0 line 287
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3118 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw3119 line 298
  61. def OAI.MUB6.Certificate.PairSemantics.raw3119step0 line 300
  62. def OAI.MUB6.Certificate.PairSemantics.raw3119step1 line 302
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical3119 line 304
  64. def OAI.MUB6.Certificate.PairSemantics.raw3120 line 317
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3120 line 319
  66. def OAI.MUB6.Certificate.PairSemantics.raw3121 line 323
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical3121 line 325
  68. def OAI.MUB6.Certificate.PairSemantics.raw3122 line 329
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3122 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw3123 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw3123step0 line 337
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3123 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw3124 line 348
  74. def OAI.MUB6.Certificate.PairSemantics.raw3124step0 line 350
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3124 line 352
  76. def OAI.MUB6.Certificate.PairSemantics.raw3125 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw3125step0 line 363
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical3125 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw3126 line 374
  80. def OAI.MUB6.Certificate.PairSemantics.raw3126step0 line 376
  81. def OAI.MUB6.Certificate.PairSemantics.raw3126step1 line 378
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3126 line 380
  83. def OAI.MUB6.Certificate.PairSemantics.raw3127 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw3127step0 line 395
  85. def OAI.MUB6.Certificate.PairSemantics.raw3127step1 line 397
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3127 line 399
  87. def OAI.MUB6.Certificate.PairSemantics.raw3128 line 412
  88. def OAI.MUB6.Certificate.PairSemantics.raw3128step0 line 414
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3128 line 416
  90. def OAI.MUB6.Certificate.PairSemantics.raw3129 line 425
  91. def OAI.MUB6.Certificate.PairSemantics.raw3129step0 line 427
  92. def OAI.MUB6.Certificate.PairSemantics.raw3129step1 line 429
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3129 line 431
  94. def OAI.MUB6.Certificate.PairSemantics.raw3130 line 444
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical3130 line 446
  96. def OAI.MUB6.Certificate.PairSemantics.raw3131 line 450
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3131 line 452
  98. def OAI.MUB6.Certificate.PairSemantics.raw3132 line 456
  99. def OAI.MUB6.Certificate.PairSemantics.raw3132step0 line 458
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3132 line 460
  101. def OAI.MUB6.Certificate.PairSemantics.raw3133 line 469
  102. def OAI.MUB6.Certificate.PairSemantics.raw3133step0 line 471
  103. def OAI.MUB6.Certificate.PairSemantics.raw3133step1 line 473
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3133 line 475
  105. def OAI.MUB6.Certificate.PairSemantics.raw3134 line 488
  106. def OAI.MUB6.Certificate.PairSemantics.raw3134step0 line 490
  107. def OAI.MUB6.Certificate.PairSemantics.raw3134step1 line 492
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical3134 line 494
  109. def OAI.MUB6.Certificate.PairSemantics.raw3135 line 507
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical3135 line 509