OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical20.lean

GitHub source file

114 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw640 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw640step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical640 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw641 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw641step0 line 33
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical641 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw642 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw642step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical642 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw643 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw643step0 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical643 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw644 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw644step0 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw644step1 line 74
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical644 line 76
  17. def OAI.MUB6.Certificate.PairSemantics.raw645 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw645step0 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw645step1 line 93
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical645 line 95
  21. def OAI.MUB6.Certificate.PairSemantics.raw646 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw646step0 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical646 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw647 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw647step0 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw647step1 line 125
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical647 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw648 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw648step0 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw648step1 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical648 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw649 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw649step0 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw649step1 line 163
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical649 line 165
  36. def OAI.MUB6.Certificate.PairSemantics.raw650 line 178
  37. def OAI.MUB6.Certificate.PairSemantics.raw650step0 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw650step1 line 182
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical650 line 184
  40. def OAI.MUB6.Certificate.PairSemantics.raw651 line 197
  41. def OAI.MUB6.Certificate.PairSemantics.raw651step0 line 199
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical651 line 201
  43. def OAI.MUB6.Certificate.PairSemantics.raw652 line 210
  44. def OAI.MUB6.Certificate.PairSemantics.raw652step0 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw652step1 line 214
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical652 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw653 line 229
  48. def OAI.MUB6.Certificate.PairSemantics.raw653step0 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw653step1 line 233
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical653 line 235
  51. def OAI.MUB6.Certificate.PairSemantics.raw654 line 248
  52. def OAI.MUB6.Certificate.PairSemantics.raw654step0 line 250
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical654 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw655 line 261
  55. def OAI.MUB6.Certificate.PairSemantics.raw655step0 line 263
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical655 line 265
  57. def OAI.MUB6.Certificate.PairSemantics.raw656 line 274
  58. def OAI.MUB6.Certificate.PairSemantics.raw656step0 line 276
  59. def OAI.MUB6.Certificate.PairSemantics.raw656step1 line 278
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical656 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw657 line 293
  62. def OAI.MUB6.Certificate.PairSemantics.raw657step0 line 295
  63. def OAI.MUB6.Certificate.PairSemantics.raw657step1 line 297
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical657 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw658 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw658step0 line 314
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical658 line 316
  68. def OAI.MUB6.Certificate.PairSemantics.raw659 line 325
  69. def OAI.MUB6.Certificate.PairSemantics.raw659step0 line 327
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical659 line 329
  71. def OAI.MUB6.Certificate.PairSemantics.raw660 line 338
  72. def OAI.MUB6.Certificate.PairSemantics.raw660step0 line 340
  73. def OAI.MUB6.Certificate.PairSemantics.raw660step1 line 342
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical660 line 344
  75. def OAI.MUB6.Certificate.PairSemantics.raw661 line 357
  76. def OAI.MUB6.Certificate.PairSemantics.raw661step0 line 359
  77. def OAI.MUB6.Certificate.PairSemantics.raw661step1 line 361
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical661 line 363
  79. def OAI.MUB6.Certificate.PairSemantics.raw662 line 376
  80. def OAI.MUB6.Certificate.PairSemantics.raw662step0 line 378
  81. def OAI.MUB6.Certificate.PairSemantics.raw662step1 line 380
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical662 line 382
  83. def OAI.MUB6.Certificate.PairSemantics.raw663 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw663step0 line 397
  85. def OAI.MUB6.Certificate.PairSemantics.raw663step1 line 399
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical663 line 401
  87. def OAI.MUB6.Certificate.PairSemantics.raw664 line 414
  88. def OAI.MUB6.Certificate.PairSemantics.raw664step0 line 416
  89. def OAI.MUB6.Certificate.PairSemantics.raw664step1 line 418
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical664 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw665 line 433
  92. def OAI.MUB6.Certificate.PairSemantics.raw665step0 line 435
  93. def OAI.MUB6.Certificate.PairSemantics.raw665step1 line 437
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical665 line 439
  95. def OAI.MUB6.Certificate.PairSemantics.raw666 line 452
  96. def OAI.MUB6.Certificate.PairSemantics.raw666step0 line 454
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical666 line 456
  98. def OAI.MUB6.Certificate.PairSemantics.raw667 line 465
  99. def OAI.MUB6.Certificate.PairSemantics.raw667step0 line 467
  100. def OAI.MUB6.Certificate.PairSemantics.raw667step1 line 469
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical667 line 471
  102. def OAI.MUB6.Certificate.PairSemantics.raw668 line 484
  103. def OAI.MUB6.Certificate.PairSemantics.raw668step0 line 486
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical668 line 488
  105. def OAI.MUB6.Certificate.PairSemantics.raw669 line 497
  106. def OAI.MUB6.Certificate.PairSemantics.raw669step0 line 499
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical669 line 501
  108. def OAI.MUB6.Certificate.PairSemantics.raw670 line 510
  109. def OAI.MUB6.Certificate.PairSemantics.raw670step0 line 512
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical670 line 514
  111. def OAI.MUB6.Certificate.PairSemantics.raw671 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw671step0 line 525
  113. def OAI.MUB6.Certificate.PairSemantics.raw671step1 line 527
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical671 line 529