OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical142.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4544 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw4544step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw4544step1 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw4544step2 line 23
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4544 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw4545 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw4545step0 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw4545step1 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw4545step2 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4545 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw4546 line 69
  12. def OAI.MUB6.Certificate.PairSemantics.raw4546step0 line 71
  13. def OAI.MUB6.Certificate.PairSemantics.raw4546step1 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw4546step2 line 75
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical4546 line 77
  16. def OAI.MUB6.Certificate.PairSemantics.raw4547 line 95
  17. def OAI.MUB6.Certificate.PairSemantics.raw4547step0 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw4547step1 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw4547step2 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw4547step3 line 103
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4547 line 105
  22. def OAI.MUB6.Certificate.PairSemantics.raw4548 line 127
  23. def OAI.MUB6.Certificate.PairSemantics.raw4548step0 line 129
  24. def OAI.MUB6.Certificate.PairSemantics.raw4548step1 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw4548step2 line 133
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4548 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw4549 line 153
  28. def OAI.MUB6.Certificate.PairSemantics.raw4549step0 line 155
  29. def OAI.MUB6.Certificate.PairSemantics.raw4549step1 line 157
  30. def OAI.MUB6.Certificate.PairSemantics.raw4549step2 line 159
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4549 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw4550 line 179
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4550 line 181
  34. def OAI.MUB6.Certificate.PairSemantics.raw4551 line 185
  35. def OAI.MUB6.Certificate.PairSemantics.raw4551step0 line 187
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4551 line 189
  37. def OAI.MUB6.Certificate.PairSemantics.raw4552 line 198
  38. def OAI.MUB6.Certificate.PairSemantics.raw4552step0 line 200
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4552 line 202
  40. def OAI.MUB6.Certificate.PairSemantics.raw4553 line 211
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical4553 line 213
  42. def OAI.MUB6.Certificate.PairSemantics.raw4554 line 217
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4554 line 219
  44. def OAI.MUB6.Certificate.PairSemantics.raw4555 line 223
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical4555 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw4556 line 229
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4556 line 231
  48. def OAI.MUB6.Certificate.PairSemantics.raw4557 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw4557step0 line 237
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4557 line 239
  51. def OAI.MUB6.Certificate.PairSemantics.raw4558 line 248
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4558 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw4559 line 254
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4559 line 256
  55. def OAI.MUB6.Certificate.PairSemantics.raw4560 line 260
  56. def OAI.MUB6.Certificate.PairSemantics.raw4560step0 line 262
  57. def OAI.MUB6.Certificate.PairSemantics.raw4560step1 line 264
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4560 line 266
  59. def OAI.MUB6.Certificate.PairSemantics.raw4561 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw4561step0 line 281
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4561 line 283
  62. def OAI.MUB6.Certificate.PairSemantics.raw4562 line 292
  63. def OAI.MUB6.Certificate.PairSemantics.raw4562step0 line 294
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4562 line 296
  65. def OAI.MUB6.Certificate.PairSemantics.raw4563 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw4563step0 line 307
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4563 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw4564 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw4564step0 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw4564step1 line 322
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4564 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw4565 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw4565step0 line 339
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4565 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw4566 line 350
  76. def OAI.MUB6.Certificate.PairSemantics.raw4566step0 line 352
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4566 line 354
  78. def OAI.MUB6.Certificate.PairSemantics.raw4567 line 363
  79. def OAI.MUB6.Certificate.PairSemantics.raw4567step0 line 365
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4567 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw4568 line 376
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4568 line 378
  83. def OAI.MUB6.Certificate.PairSemantics.raw4569 line 382
  84. def OAI.MUB6.Certificate.PairSemantics.raw4569step0 line 384
  85. def OAI.MUB6.Certificate.PairSemantics.raw4569step1 line 386
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4569 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw4570 line 401
  88. def OAI.MUB6.Certificate.PairSemantics.raw4570step0 line 403
  89. def OAI.MUB6.Certificate.PairSemantics.raw4570step1 line 405
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4570 line 407
  91. def OAI.MUB6.Certificate.PairSemantics.raw4571 line 420
  92. def OAI.MUB6.Certificate.PairSemantics.raw4571step0 line 422
  93. def OAI.MUB6.Certificate.PairSemantics.raw4571step1 line 424
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4571 line 426
  95. def OAI.MUB6.Certificate.PairSemantics.raw4572 line 439
  96. def OAI.MUB6.Certificate.PairSemantics.raw4572step0 line 441
  97. def OAI.MUB6.Certificate.PairSemantics.raw4572step1 line 443
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical4572 line 445
  99. def OAI.MUB6.Certificate.PairSemantics.raw4573 line 458
  100. def OAI.MUB6.Certificate.PairSemantics.raw4573step0 line 460
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4573 line 462
  102. def OAI.MUB6.Certificate.PairSemantics.raw4574 line 471
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4574 line 473
  104. def OAI.MUB6.Certificate.PairSemantics.raw4575 line 477
  105. def OAI.MUB6.Certificate.PairSemantics.raw4575step0 line 479
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical4575 line 481