OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical95.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3040 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw3040step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw3040step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3040 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw3041 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw3041step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw3041step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3041 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw3042 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw3042step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw3042step1 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw3042step2 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3042 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw3043 line 85
  15. def OAI.MUB6.Certificate.PairSemantics.raw3043step0 line 87
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3043 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw3044 line 98
  18. def OAI.MUB6.Certificate.PairSemantics.raw3044step0 line 100
  19. def OAI.MUB6.Certificate.PairSemantics.raw3044step1 line 102
  20. def OAI.MUB6.Certificate.PairSemantics.raw3044step2 line 104
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3044 line 106
  22. def OAI.MUB6.Certificate.PairSemantics.raw3045 line 123
  23. def OAI.MUB6.Certificate.PairSemantics.raw3045step0 line 125
  24. def OAI.MUB6.Certificate.PairSemantics.raw3045step1 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw3045step2 line 129
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3045 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw3046 line 148
  28. def OAI.MUB6.Certificate.PairSemantics.raw3046step0 line 150
  29. def OAI.MUB6.Certificate.PairSemantics.raw3046step1 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw3046step2 line 154
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3046 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw3047 line 173
  33. def OAI.MUB6.Certificate.PairSemantics.raw3047step0 line 175
  34. def OAI.MUB6.Certificate.PairSemantics.raw3047step1 line 177
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3047 line 179
  36. def OAI.MUB6.Certificate.PairSemantics.raw3048 line 192
  37. def OAI.MUB6.Certificate.PairSemantics.raw3048step0 line 194
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3048 line 196
  39. def OAI.MUB6.Certificate.PairSemantics.raw3049 line 205
  40. def OAI.MUB6.Certificate.PairSemantics.raw3049step0 line 207
  41. def OAI.MUB6.Certificate.PairSemantics.raw3049step1 line 209
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3049 line 211
  43. def OAI.MUB6.Certificate.PairSemantics.raw3050 line 224
  44. def OAI.MUB6.Certificate.PairSemantics.raw3050step0 line 226
  45. def OAI.MUB6.Certificate.PairSemantics.raw3050step1 line 228
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3050 line 230
  47. def OAI.MUB6.Certificate.PairSemantics.raw3051 line 243
  48. def OAI.MUB6.Certificate.PairSemantics.raw3051step0 line 245
  49. def OAI.MUB6.Certificate.PairSemantics.raw3051step1 line 247
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3051 line 249
  51. def OAI.MUB6.Certificate.PairSemantics.raw3052 line 262
  52. def OAI.MUB6.Certificate.PairSemantics.raw3052step0 line 264
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3052 line 266
  54. def OAI.MUB6.Certificate.PairSemantics.raw3053 line 275
  55. def OAI.MUB6.Certificate.PairSemantics.raw3053step0 line 277
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3053 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw3054 line 288
  58. def OAI.MUB6.Certificate.PairSemantics.raw3054step0 line 290
  59. def OAI.MUB6.Certificate.PairSemantics.raw3054step1 line 292
  60. def OAI.MUB6.Certificate.PairSemantics.raw3054step2 line 294
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3054 line 296
  62. def OAI.MUB6.Certificate.PairSemantics.raw3055 line 313
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical3055 line 315
  64. def OAI.MUB6.Certificate.PairSemantics.raw3056 line 319
  65. def OAI.MUB6.Certificate.PairSemantics.raw3056step0 line 321
  66. def OAI.MUB6.Certificate.PairSemantics.raw3056step1 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw3056step2 line 325
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3056 line 327
  69. def OAI.MUB6.Certificate.PairSemantics.raw3057 line 344
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3057 line 346
  71. def OAI.MUB6.Certificate.PairSemantics.raw3058 line 350
  72. def OAI.MUB6.Certificate.PairSemantics.raw3058step0 line 352
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3058 line 354
  74. def OAI.MUB6.Certificate.PairSemantics.raw3059 line 363
  75. def OAI.MUB6.Certificate.PairSemantics.raw3059step0 line 365
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3059 line 367
  77. def OAI.MUB6.Certificate.PairSemantics.raw3060 line 376
  78. def OAI.MUB6.Certificate.PairSemantics.raw3060step0 line 378
  79. def OAI.MUB6.Certificate.PairSemantics.raw3060step1 line 380
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3060 line 382
  81. def OAI.MUB6.Certificate.PairSemantics.raw3061 line 395
  82. def OAI.MUB6.Certificate.PairSemantics.raw3061step0 line 397
  83. def OAI.MUB6.Certificate.PairSemantics.raw3061step1 line 399
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3061 line 401
  85. def OAI.MUB6.Certificate.PairSemantics.raw3062 line 414
  86. def OAI.MUB6.Certificate.PairSemantics.raw3062step0 line 416
  87. def OAI.MUB6.Certificate.PairSemantics.raw3062step1 line 418
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical3062 line 420
  89. def OAI.MUB6.Certificate.PairSemantics.raw3063 line 433
  90. def OAI.MUB6.Certificate.PairSemantics.raw3063step0 line 435
  91. def OAI.MUB6.Certificate.PairSemantics.raw3063step1 line 437
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3063 line 439
  93. def OAI.MUB6.Certificate.PairSemantics.raw3064 line 452
  94. def OAI.MUB6.Certificate.PairSemantics.raw3064step0 line 454
  95. def OAI.MUB6.Certificate.PairSemantics.raw3064step1 line 456
  96. def OAI.MUB6.Certificate.PairSemantics.raw3064step2 line 458
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3064 line 460
  98. def OAI.MUB6.Certificate.PairSemantics.raw3065 line 477
  99. def OAI.MUB6.Certificate.PairSemantics.raw3065step0 line 479
  100. def OAI.MUB6.Certificate.PairSemantics.raw3065step1 line 481
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3065 line 483
  102. def OAI.MUB6.Certificate.PairSemantics.raw3066 line 496
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3066 line 498
  104. def OAI.MUB6.Certificate.PairSemantics.raw3067 line 502
  105. def OAI.MUB6.Certificate.PairSemantics.raw3067step0 line 504
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical3067 line 506
  107. def OAI.MUB6.Certificate.PairSemantics.raw3068 line 515
  108. def OAI.MUB6.Certificate.PairSemantics.raw3068step0 line 517
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3068 line 519
  110. def OAI.MUB6.Certificate.PairSemantics.raw3069 line 528
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical3069 line 530
  112. def OAI.MUB6.Certificate.PairSemantics.raw3070 line 534
  113. def OAI.MUB6.Certificate.PairSemantics.raw3070step0 line 536
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical3070 line 538
  115. def OAI.MUB6.Certificate.PairSemantics.raw3071 line 547
  116. def OAI.MUB6.Certificate.PairSemantics.raw3071step0 line 549
  117. def OAI.MUB6.Certificate.PairSemantics.raw3071step1 line 551
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical3071 line 553