OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical232.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7424 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw7424step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical7424 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw7425 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw7425step0 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical7425 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw7426 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw7426step0 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7426 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw7427 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw7427step0 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw7427step1 line 59
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7427 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw7428 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw7428step0 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw7428step1 line 78
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7428 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw7429 line 93
  19. def OAI.MUB6.Certificate.PairSemantics.raw7429step0 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw7429step1 line 97
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7429 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw7430 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw7430step0 line 114
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical7430 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw7431 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw7431step0 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw7431step1 line 129
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7431 line 131
  29. def OAI.MUB6.Certificate.PairSemantics.raw7432 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw7432step0 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw7432step1 line 148
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7432 line 150
  33. def OAI.MUB6.Certificate.PairSemantics.raw7433 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw7433step0 line 165
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7433 line 167
  36. def OAI.MUB6.Certificate.PairSemantics.raw7434 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw7434step0 line 178
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7434 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw7435 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw7435step0 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw7435step1 line 193
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7435 line 195
  43. def OAI.MUB6.Certificate.PairSemantics.raw7436 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw7436step0 line 211
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7436 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw7437 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw7437step0 line 224
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7437 line 226
  49. def OAI.MUB6.Certificate.PairSemantics.raw7438 line 235
  50. def OAI.MUB6.Certificate.PairSemantics.raw7438step0 line 237
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical7438 line 239
  52. def OAI.MUB6.Certificate.PairSemantics.raw7439 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw7439step0 line 250
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7439 line 252
  55. def OAI.MUB6.Certificate.PairSemantics.raw7440 line 261
  56. def OAI.MUB6.Certificate.PairSemantics.raw7440step0 line 263
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7440 line 265
  58. def OAI.MUB6.Certificate.PairSemantics.raw7441 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw7441step0 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw7441step1 line 279
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7441 line 281
  62. def OAI.MUB6.Certificate.PairSemantics.raw7442 line 294
  63. def OAI.MUB6.Certificate.PairSemantics.raw7442step0 line 296
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical7442 line 298
  65. def OAI.MUB6.Certificate.PairSemantics.raw7443 line 307
  66. def OAI.MUB6.Certificate.PairSemantics.raw7443step0 line 309
  67. def OAI.MUB6.Certificate.PairSemantics.raw7443step1 line 311
  68. def OAI.MUB6.Certificate.PairSemantics.raw7443step2 line 313
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7443 line 315
  70. def OAI.MUB6.Certificate.PairSemantics.raw7444 line 333
  71. def OAI.MUB6.Certificate.PairSemantics.raw7444step0 line 335
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7444 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw7445 line 346
  74. def OAI.MUB6.Certificate.PairSemantics.raw7445step0 line 348
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7445 line 350
  76. def OAI.MUB6.Certificate.PairSemantics.raw7446 line 359
  77. def OAI.MUB6.Certificate.PairSemantics.raw7446step0 line 361
  78. def OAI.MUB6.Certificate.PairSemantics.raw7446step1 line 363
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical7446 line 365
  80. def OAI.MUB6.Certificate.PairSemantics.raw7447 line 378
  81. def OAI.MUB6.Certificate.PairSemantics.raw7447step0 line 380
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7447 line 382
  83. def OAI.MUB6.Certificate.PairSemantics.raw7448 line 391
  84. def OAI.MUB6.Certificate.PairSemantics.raw7448step0 line 393
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7448 line 395
  86. def OAI.MUB6.Certificate.PairSemantics.raw7449 line 404
  87. def OAI.MUB6.Certificate.PairSemantics.raw7449step0 line 406
  88. def OAI.MUB6.Certificate.PairSemantics.raw7449step1 line 408
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7449 line 410
  90. def OAI.MUB6.Certificate.PairSemantics.raw7450 line 423
  91. def OAI.MUB6.Certificate.PairSemantics.raw7450step0 line 425
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7450 line 427
  93. def OAI.MUB6.Certificate.PairSemantics.raw7451 line 436
  94. def OAI.MUB6.Certificate.PairSemantics.raw7451step0 line 438
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7451 line 440
  96. def OAI.MUB6.Certificate.PairSemantics.raw7452 line 449
  97. def OAI.MUB6.Certificate.PairSemantics.raw7452step0 line 451
  98. def OAI.MUB6.Certificate.PairSemantics.raw7452step1 line 453
  99. def OAI.MUB6.Certificate.PairSemantics.raw7452step2 line 455
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical7452 line 457
  101. def OAI.MUB6.Certificate.PairSemantics.raw7453 line 475
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical7453 line 477
  103. def OAI.MUB6.Certificate.PairSemantics.raw7454 line 481
  104. def OAI.MUB6.Certificate.PairSemantics.raw7454step0 line 483
  105. def OAI.MUB6.Certificate.PairSemantics.raw7454step1 line 485
  106. def OAI.MUB6.Certificate.PairSemantics.raw7454step2 line 487
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7454 line 489
  108. def OAI.MUB6.Certificate.PairSemantics.raw7455 line 507
  109. def OAI.MUB6.Certificate.PairSemantics.raw7455step0 line 509
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical7455 line 511