OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical260.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8320 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw8320step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw8320step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8320 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw8321 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw8321step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw8321step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8321 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw8322 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw8322step0 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw8322step1 line 63
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8322 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw8323 line 78
  14. def OAI.MUB6.Certificate.PairSemantics.raw8323step0 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw8323step1 line 82
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8323 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw8324 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw8324step0 line 99
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8324 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw8325 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw8325step0 line 112
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical8325 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw8326 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw8326step0 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8326 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw8327 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw8327step0 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw8327step1 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8327 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw8328 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw8328step0 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw8328step1 line 159
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8328 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw8329 line 174
  35. def OAI.MUB6.Certificate.PairSemantics.raw8329step0 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw8329step1 line 178
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8329 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw8330 line 193
  39. def OAI.MUB6.Certificate.PairSemantics.raw8330step0 line 195
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8330 line 197
  41. def OAI.MUB6.Certificate.PairSemantics.raw8331 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw8331step0 line 208
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical8331 line 210
  44. def OAI.MUB6.Certificate.PairSemantics.raw8332 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw8332step0 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw8332step1 line 223
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8332 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw8333 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw8333step0 line 240
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8333 line 242
  51. def OAI.MUB6.Certificate.PairSemantics.raw8334 line 251
  52. def OAI.MUB6.Certificate.PairSemantics.raw8334step0 line 253
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8334 line 255
  54. def OAI.MUB6.Certificate.PairSemantics.raw8335 line 264
  55. def OAI.MUB6.Certificate.PairSemantics.raw8335step0 line 266
  56. def OAI.MUB6.Certificate.PairSemantics.raw8335step1 line 268
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8335 line 270
  58. def OAI.MUB6.Certificate.PairSemantics.raw8336 line 283
  59. def OAI.MUB6.Certificate.PairSemantics.raw8336step0 line 285
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8336 line 287
  61. def OAI.MUB6.Certificate.PairSemantics.raw8337 line 296
  62. def OAI.MUB6.Certificate.PairSemantics.raw8337step0 line 298
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical8337 line 300
  64. def OAI.MUB6.Certificate.PairSemantics.raw8338 line 310
  65. def OAI.MUB6.Certificate.PairSemantics.raw8338step0 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw8338step1 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw8338step2 line 316
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8338 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw8339 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw8339step0 line 338
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8339 line 340
  72. def OAI.MUB6.Certificate.PairSemantics.raw8340 line 349
  73. def OAI.MUB6.Certificate.PairSemantics.raw8340step0 line 351
  74. def OAI.MUB6.Certificate.PairSemantics.raw8340step1 line 353
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8340 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw8341 line 368
  77. def OAI.MUB6.Certificate.PairSemantics.raw8341step0 line 370
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical8341 line 372
  79. def OAI.MUB6.Certificate.PairSemantics.raw8342 line 381
  80. def OAI.MUB6.Certificate.PairSemantics.raw8342step0 line 383
  81. def OAI.MUB6.Certificate.PairSemantics.raw8342step1 line 385
  82. def OAI.MUB6.Certificate.PairSemantics.raw8342step2 line 387
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8342 line 389
  84. def OAI.MUB6.Certificate.PairSemantics.raw8343 line 407
  85. def OAI.MUB6.Certificate.PairSemantics.raw8343step0 line 409
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8343 line 411
  87. def OAI.MUB6.Certificate.PairSemantics.raw8344 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw8344step0 line 422
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8344 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw8345 line 433
  91. def OAI.MUB6.Certificate.PairSemantics.raw8345step0 line 435
  92. def OAI.MUB6.Certificate.PairSemantics.raw8345step1 line 437
  93. def OAI.MUB6.Certificate.PairSemantics.raw8345step2 line 439
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8345 line 441
  95. def OAI.MUB6.Certificate.PairSemantics.raw8346 line 458
  96. def OAI.MUB6.Certificate.PairSemantics.raw8346step0 line 460
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical8346 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw8347 line 471
  99. def OAI.MUB6.Certificate.PairSemantics.raw8347step0 line 473
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical8347 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw8348 line 484
  102. def OAI.MUB6.Certificate.PairSemantics.raw8348step0 line 486
  103. def OAI.MUB6.Certificate.PairSemantics.raw8348step1 line 488
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8348 line 490
  105. def OAI.MUB6.Certificate.PairSemantics.raw8349 line 503
  106. def OAI.MUB6.Certificate.PairSemantics.raw8349step0 line 505
  107. def OAI.MUB6.Certificate.PairSemantics.raw8349step1 line 507
  108. def OAI.MUB6.Certificate.PairSemantics.raw8349step2 line 509
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical8349 line 511
  110. def OAI.MUB6.Certificate.PairSemantics.raw8350 line 528
  111. def OAI.MUB6.Certificate.PairSemantics.raw8350step0 line 530
  112. def OAI.MUB6.Certificate.PairSemantics.raw8350step1 line 532
  113. def OAI.MUB6.Certificate.PairSemantics.raw8350step2 line 534
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical8350 line 536
  115. def OAI.MUB6.Certificate.PairSemantics.raw8351 line 553
  116. def OAI.MUB6.Certificate.PairSemantics.raw8351step0 line 555
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical8351 line 557