OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical79.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2528 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw2528step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw2528step1 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw2528step2 line 23
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2528 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw2529 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw2529step0 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw2529step1 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2529 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw2530 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw2530step0 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw2530step1 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw2530step2 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical2530 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw2531 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw2531step0 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw2531step1 line 90
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2531 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw2532 line 105
  20. def OAI.MUB6.Certificate.PairSemantics.raw2532step0 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw2532step1 line 109
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2532 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw2533 line 124
  24. def OAI.MUB6.Certificate.PairSemantics.raw2533step0 line 126
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2533 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw2534 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw2534step0 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw2534step1 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw2534step2 line 143
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2534 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw2535 line 162
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2535 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw2536 line 168
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2536 line 170
  35. def OAI.MUB6.Certificate.PairSemantics.raw2537 line 174
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2537 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw2538 line 180
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical2538 line 182
  39. def OAI.MUB6.Certificate.PairSemantics.raw2539 line 186
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2539 line 188
  41. def OAI.MUB6.Certificate.PairSemantics.raw2540 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw2540step0 line 194
  43. def OAI.MUB6.Certificate.PairSemantics.raw2540step1 line 196
  44. def OAI.MUB6.Certificate.PairSemantics.raw2540step2 line 198
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2540 line 200
  46. def OAI.MUB6.Certificate.PairSemantics.raw2541 line 217
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical2541 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw2542 line 223
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2542 line 225
  50. def OAI.MUB6.Certificate.PairSemantics.raw2543 line 229
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2543 line 231
  52. def OAI.MUB6.Certificate.PairSemantics.raw2544 line 235
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2544 line 237
  54. def OAI.MUB6.Certificate.PairSemantics.raw2545 line 241
  55. def OAI.MUB6.Certificate.PairSemantics.raw2545step0 line 243
  56. def OAI.MUB6.Certificate.PairSemantics.raw2545step1 line 245
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2545 line 247
  58. def OAI.MUB6.Certificate.PairSemantics.raw2546 line 260
  59. def OAI.MUB6.Certificate.PairSemantics.raw2546step0 line 262
  60. def OAI.MUB6.Certificate.PairSemantics.raw2546step1 line 264
  61. def OAI.MUB6.Certificate.PairSemantics.raw2546step2 line 266
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2546 line 268
  63. def OAI.MUB6.Certificate.PairSemantics.raw2547 line 285
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2547 line 287
  65. def OAI.MUB6.Certificate.PairSemantics.raw2548 line 291
  66. def OAI.MUB6.Certificate.PairSemantics.raw2548step0 line 293
  67. def OAI.MUB6.Certificate.PairSemantics.raw2548step1 line 295
  68. def OAI.MUB6.Certificate.PairSemantics.raw2548step2 line 297
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2548 line 299
  70. def OAI.MUB6.Certificate.PairSemantics.raw2549 line 316
  71. def OAI.MUB6.Certificate.PairSemantics.raw2549step0 line 318
  72. def OAI.MUB6.Certificate.PairSemantics.raw2549step1 line 320
  73. def OAI.MUB6.Certificate.PairSemantics.raw2549step2 line 322
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2549 line 324
  75. def OAI.MUB6.Certificate.PairSemantics.raw2550 line 341
  76. def OAI.MUB6.Certificate.PairSemantics.raw2550step0 line 343
  77. def OAI.MUB6.Certificate.PairSemantics.raw2550step1 line 345
  78. def OAI.MUB6.Certificate.PairSemantics.raw2550step2 line 347
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2550 line 349
  80. def OAI.MUB6.Certificate.PairSemantics.raw2551 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw2551step0 line 368
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2551 line 370
  83. def OAI.MUB6.Certificate.PairSemantics.raw2552 line 379
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2552 line 381
  85. def OAI.MUB6.Certificate.PairSemantics.raw2553 line 385
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2553 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw2554 line 391
  88. def OAI.MUB6.Certificate.PairSemantics.raw2554step0 line 393
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2554 line 395
  90. def OAI.MUB6.Certificate.PairSemantics.raw2555 line 404
  91. def OAI.MUB6.Certificate.PairSemantics.raw2555step0 line 406
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2555 line 408
  93. def OAI.MUB6.Certificate.PairSemantics.raw2556 line 417
  94. def OAI.MUB6.Certificate.PairSemantics.raw2556step0 line 419
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical2556 line 421
  96. def OAI.MUB6.Certificate.PairSemantics.raw2557 line 430
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2557 line 432
  98. def OAI.MUB6.Certificate.PairSemantics.raw2558 line 436
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical2558 line 438
  100. def OAI.MUB6.Certificate.PairSemantics.raw2559 line 442
  101. def OAI.MUB6.Certificate.PairSemantics.raw2559step0 line 444
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical2559 line 446