OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical2.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw64 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw64step0 line 22
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical64 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw65 line 33
  5. def OAI.MUB6.Certificate.PairSemantics.raw65step0 line 35
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical65 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw66 line 46
  8. def OAI.MUB6.Certificate.PairSemantics.raw66step0 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical66 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw67 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw67step0 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical67 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw68 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw68step0 line 74
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical68 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw69 line 85
  17. def OAI.MUB6.Certificate.PairSemantics.raw69step0 line 87
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical69 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw70 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw70step0 line 100
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical70 line 102
  22. def OAI.MUB6.Certificate.PairSemantics.raw71 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw71step0 line 113
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical71 line 115
  25. def OAI.MUB6.Certificate.PairSemantics.raw72 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw72step0 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw72step1 line 128
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical72 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw73 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw73step0 line 145
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical73 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw74 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw74step0 line 158
  34. def OAI.MUB6.Certificate.PairSemantics.raw74step1 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw74step2 line 162
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical74 line 164
  37. def OAI.MUB6.Certificate.PairSemantics.raw75 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw75step0 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw75step1 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw75step2 line 187
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical75 line 189
  42. def OAI.MUB6.Certificate.PairSemantics.raw76 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw76step0 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw76step1 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical76 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw77 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw77step0 line 227
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical77 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw78 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw78step0 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw78step1 line 242
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical78 line 244
  53. def OAI.MUB6.Certificate.PairSemantics.raw79 line 257
  54. def OAI.MUB6.Certificate.PairSemantics.raw79step0 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw79step1 line 261
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical79 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw80 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw80step0 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw80step1 line 280
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical80 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw81 line 295
  62. def OAI.MUB6.Certificate.PairSemantics.raw81step0 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw81step1 line 299
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical81 line 301
  65. def OAI.MUB6.Certificate.PairSemantics.raw82 line 314
  66. def OAI.MUB6.Certificate.PairSemantics.raw82step0 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw82step1 line 318
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical82 line 320
  69. def OAI.MUB6.Certificate.PairSemantics.raw83 line 333
  70. def OAI.MUB6.Certificate.PairSemantics.raw83step0 line 335
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical83 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw84 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw84step0 line 348
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical84 line 350
  75. def OAI.MUB6.Certificate.PairSemantics.raw85 line 359
  76. def OAI.MUB6.Certificate.PairSemantics.raw85step0 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw85step1 line 363
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical85 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw86 line 378
  80. def OAI.MUB6.Certificate.PairSemantics.raw86step0 line 380
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical86 line 382
  82. def OAI.MUB6.Certificate.PairSemantics.raw87 line 391
  83. def OAI.MUB6.Certificate.PairSemantics.raw87step0 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw87step1 line 395
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical87 line 397
  86. def OAI.MUB6.Certificate.PairSemantics.raw88 line 410
  87. def OAI.MUB6.Certificate.PairSemantics.raw88step0 line 412
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical88 line 414
  89. def OAI.MUB6.Certificate.PairSemantics.raw89 line 423
  90. def OAI.MUB6.Certificate.PairSemantics.raw89step0 line 425
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical89 line 427
  92. def OAI.MUB6.Certificate.PairSemantics.raw90 line 436
  93. def OAI.MUB6.Certificate.PairSemantics.raw90step0 line 438
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical90 line 440
  95. def OAI.MUB6.Certificate.PairSemantics.raw91 line 449
  96. def OAI.MUB6.Certificate.PairSemantics.raw91step0 line 451
  97. def OAI.MUB6.Certificate.PairSemantics.raw91step1 line 453
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical91 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw92 line 468
  100. def OAI.MUB6.Certificate.PairSemantics.raw92step0 line 470
  101. def OAI.MUB6.Certificate.PairSemantics.raw92step1 line 472
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical92 line 474
  103. def OAI.MUB6.Certificate.PairSemantics.raw93 line 487
  104. def OAI.MUB6.Certificate.PairSemantics.raw93step0 line 489
  105. def OAI.MUB6.Certificate.PairSemantics.raw93step1 line 491
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical93 line 493
  107. def OAI.MUB6.Certificate.PairSemantics.raw94 line 506
  108. def OAI.MUB6.Certificate.PairSemantics.raw94step0 line 508
  109. def OAI.MUB6.Certificate.PairSemantics.raw94step1 line 510
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical94 line 512
  111. def OAI.MUB6.Certificate.PairSemantics.raw95 line 525
  112. def OAI.MUB6.Certificate.PairSemantics.raw95step0 line 527
  113. def OAI.MUB6.Certificate.PairSemantics.raw95step1 line 529
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical95 line 531