OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical169.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5408 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw5408step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw5408step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5408 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw5409 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw5409step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw5409step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5409 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw5410 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw5410step0 line 61
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5410 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw5411 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw5411step0 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw5411step1 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5411 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw5412 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw5412step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw5412step1 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5412 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw5413 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw5413step0 line 112
  22. def OAI.MUB6.Certificate.PairSemantics.raw5413step1 line 114
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5413 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw5414 line 129
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5414 line 131
  26. def OAI.MUB6.Certificate.PairSemantics.raw5415 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw5415step0 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw5415step1 line 139
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5415 line 141
  30. def OAI.MUB6.Certificate.PairSemantics.raw5416 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw5416step0 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw5416step1 line 158
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5416 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw5417 line 173
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5417 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw5418 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw5418step0 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw5418step1 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw5418step2 line 185
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5418 line 187
  41. def OAI.MUB6.Certificate.PairSemantics.raw5419 line 205
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5419 line 207
  43. def OAI.MUB6.Certificate.PairSemantics.raw5420 line 211
  44. def OAI.MUB6.Certificate.PairSemantics.raw5420step0 line 213
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5420 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw5421 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw5421step0 line 226
  48. def OAI.MUB6.Certificate.PairSemantics.raw5421step1 line 228
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5421 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw5422 line 243
  51. def OAI.MUB6.Certificate.PairSemantics.raw5422step0 line 245
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5422 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw5423 line 256
  54. def OAI.MUB6.Certificate.PairSemantics.raw5423step0 line 258
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5423 line 260
  56. def OAI.MUB6.Certificate.PairSemantics.raw5424 line 269
  57. def OAI.MUB6.Certificate.PairSemantics.raw5424step0 line 271
  58. def OAI.MUB6.Certificate.PairSemantics.raw5424step1 line 273
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5424 line 275
  60. def OAI.MUB6.Certificate.PairSemantics.raw5425 line 288
  61. def OAI.MUB6.Certificate.PairSemantics.raw5425step0 line 290
  62. def OAI.MUB6.Certificate.PairSemantics.raw5425step1 line 292
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5425 line 294
  64. def OAI.MUB6.Certificate.PairSemantics.raw5426 line 307
  65. def OAI.MUB6.Certificate.PairSemantics.raw5426step0 line 309
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5426 line 311
  67. def OAI.MUB6.Certificate.PairSemantics.raw5427 line 320
  68. def OAI.MUB6.Certificate.PairSemantics.raw5427step0 line 322
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5427 line 324
  70. def OAI.MUB6.Certificate.PairSemantics.raw5428 line 333
  71. def OAI.MUB6.Certificate.PairSemantics.raw5428step0 line 335
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5428 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw5429 line 346
  74. def OAI.MUB6.Certificate.PairSemantics.raw5429step0 line 348
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5429 line 350
  76. def OAI.MUB6.Certificate.PairSemantics.raw5430 line 359
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5430 line 361
  78. def OAI.MUB6.Certificate.PairSemantics.raw5431 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw5431step0 line 367
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5431 line 369
  81. def OAI.MUB6.Certificate.PairSemantics.raw5432 line 378
  82. def OAI.MUB6.Certificate.PairSemantics.raw5432step0 line 380
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5432 line 382
  84. def OAI.MUB6.Certificate.PairSemantics.raw5433 line 391
  85. def OAI.MUB6.Certificate.PairSemantics.raw5433step0 line 393
  86. def OAI.MUB6.Certificate.PairSemantics.raw5433step1 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw5433step2 line 397
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5433 line 399
  89. def OAI.MUB6.Certificate.PairSemantics.raw5434 line 417
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical5434 line 419
  91. def OAI.MUB6.Certificate.PairSemantics.raw5435 line 423
  92. def OAI.MUB6.Certificate.PairSemantics.raw5435step0 line 425
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5435 line 427
  94. def OAI.MUB6.Certificate.PairSemantics.raw5436 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw5436step0 line 438
  96. def OAI.MUB6.Certificate.PairSemantics.raw5436step1 line 440
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5436 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw5437 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw5437step0 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw5437step1 line 459
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical5437 line 461
  102. def OAI.MUB6.Certificate.PairSemantics.raw5438 line 474
  103. def OAI.MUB6.Certificate.PairSemantics.raw5438step0 line 476
  104. def OAI.MUB6.Certificate.PairSemantics.raw5438step1 line 478
  105. def OAI.MUB6.Certificate.PairSemantics.raw5438step2 line 480
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical5438 line 482
  107. def OAI.MUB6.Certificate.PairSemantics.raw5439 line 500
  108. def OAI.MUB6.Certificate.PairSemantics.raw5439step0 line 502
  109. def OAI.MUB6.Certificate.PairSemantics.raw5439step1 line 504
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5439 line 506