OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical41.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1312 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw1312step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1312step1 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw1312step2 line 22
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1312 line 24
  6. def OAI.MUB6.Certificate.PairSemantics.raw1313 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw1313step0 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw1313step1 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1313 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw1314 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw1314step0 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw1314step1 line 64
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1314 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw1315 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw1315step0 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw1315step1 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1315 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw1316 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw1316step0 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw1316step1 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1316 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw1317 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw1317step0 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw1317step1 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw1317step2 line 123
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1317 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw1318 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw1318step0 line 144
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1318 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw1319 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw1319step0 line 157
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1319 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw1320 line 168
  34. def OAI.MUB6.Certificate.PairSemantics.raw1320step0 line 170
  35. def OAI.MUB6.Certificate.PairSemantics.raw1320step1 line 172
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1320 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw1321 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw1321step0 line 189
  39. def OAI.MUB6.Certificate.PairSemantics.raw1321step1 line 191
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1321 line 193
  41. def OAI.MUB6.Certificate.PairSemantics.raw1322 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw1322step0 line 208
  43. def OAI.MUB6.Certificate.PairSemantics.raw1322step1 line 210
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1322 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw1323 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw1323step0 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw1323step1 line 229
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1323 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw1324 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw1324step0 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw1324step1 line 248
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1324 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw1325 line 263
  54. def OAI.MUB6.Certificate.PairSemantics.raw1325step0 line 265
  55. def OAI.MUB6.Certificate.PairSemantics.raw1325step1 line 267
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1325 line 269
  57. def OAI.MUB6.Certificate.PairSemantics.raw1326 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw1326step0 line 284
  59. def OAI.MUB6.Certificate.PairSemantics.raw1326step1 line 286
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1326 line 288
  61. def OAI.MUB6.Certificate.PairSemantics.raw1327 line 301
  62. def OAI.MUB6.Certificate.PairSemantics.raw1327step0 line 303
  63. def OAI.MUB6.Certificate.PairSemantics.raw1327step1 line 305
  64. def OAI.MUB6.Certificate.PairSemantics.raw1327step2 line 307
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1327 line 309
  66. def OAI.MUB6.Certificate.PairSemantics.raw1328 line 326
  67. def OAI.MUB6.Certificate.PairSemantics.raw1328step0 line 328
  68. def OAI.MUB6.Certificate.PairSemantics.raw1328step1 line 330
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1328 line 332
  70. def OAI.MUB6.Certificate.PairSemantics.raw1329 line 345
  71. def OAI.MUB6.Certificate.PairSemantics.raw1329step0 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw1329step1 line 349
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1329 line 351
  74. def OAI.MUB6.Certificate.PairSemantics.raw1330 line 364
  75. def OAI.MUB6.Certificate.PairSemantics.raw1330step0 line 366
  76. def OAI.MUB6.Certificate.PairSemantics.raw1330step1 line 368
  77. def OAI.MUB6.Certificate.PairSemantics.raw1330step2 line 370
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1330 line 372
  79. def OAI.MUB6.Certificate.PairSemantics.raw1331 line 389
  80. def OAI.MUB6.Certificate.PairSemantics.raw1331step0 line 391
  81. def OAI.MUB6.Certificate.PairSemantics.raw1331step1 line 393
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1331 line 395
  83. def OAI.MUB6.Certificate.PairSemantics.raw1332 line 408
  84. def OAI.MUB6.Certificate.PairSemantics.raw1332step0 line 410
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1332 line 412
  86. def OAI.MUB6.Certificate.PairSemantics.raw1333 line 421
  87. def OAI.MUB6.Certificate.PairSemantics.raw1333step0 line 423
  88. def OAI.MUB6.Certificate.PairSemantics.raw1333step1 line 425
  89. def OAI.MUB6.Certificate.PairSemantics.raw1333step2 line 427
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1333 line 429
  91. def OAI.MUB6.Certificate.PairSemantics.raw1334 line 446
  92. def OAI.MUB6.Certificate.PairSemantics.raw1334step0 line 448
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1334 line 450
  94. def OAI.MUB6.Certificate.PairSemantics.raw1335 line 459
  95. def OAI.MUB6.Certificate.PairSemantics.raw1335step0 line 461
  96. def OAI.MUB6.Certificate.PairSemantics.raw1335step1 line 463
  97. def OAI.MUB6.Certificate.PairSemantics.raw1335step2 line 465
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1335 line 467
  99. def OAI.MUB6.Certificate.PairSemantics.raw1336 line 484
  100. def OAI.MUB6.Certificate.PairSemantics.raw1336step0 line 486
  101. def OAI.MUB6.Certificate.PairSemantics.raw1336step1 line 488
  102. def OAI.MUB6.Certificate.PairSemantics.raw1336step2 line 490
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical1336 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw1337 line 509
  105. def OAI.MUB6.Certificate.PairSemantics.raw1337step0 line 511
  106. def OAI.MUB6.Certificate.PairSemantics.raw1337step1 line 513
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical1337 line 515
  108. def OAI.MUB6.Certificate.PairSemantics.raw1338 line 528
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical1338 line 530
  110. def OAI.MUB6.Certificate.PairSemantics.raw1339 line 534
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical1339 line 536
  112. def OAI.MUB6.Certificate.PairSemantics.raw1340 line 540
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical1340 line 542
  114. def OAI.MUB6.Certificate.PairSemantics.raw1341 line 546
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical1341 line 548
  116. def OAI.MUB6.Certificate.PairSemantics.raw1342 line 552
  117. def OAI.MUB6.Certificate.PairSemantics.raw1342step0 line 554
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical1342 line 556
  119. def OAI.MUB6.Certificate.PairSemantics.raw1343 line 565
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical1343 line 567