OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical47.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1504 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw1504step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw1504step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1504 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw1505 line 38
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1505 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw1506 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1506 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw1507 line 50
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1507 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw1508 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw1508step0 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1508 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw1509 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw1509step0 line 71
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1509 line 73
  17. def OAI.MUB6.Certificate.PairSemantics.raw1510 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw1510step0 line 84
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1510 line 86
  20. def OAI.MUB6.Certificate.PairSemantics.raw1511 line 95
  21. def OAI.MUB6.Certificate.PairSemantics.raw1511step0 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw1511step1 line 99
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1511 line 101
  24. def OAI.MUB6.Certificate.PairSemantics.raw1512 line 114
  25. def OAI.MUB6.Certificate.PairSemantics.raw1512step0 line 116
  26. def OAI.MUB6.Certificate.PairSemantics.raw1512step1 line 118
  27. def OAI.MUB6.Certificate.PairSemantics.raw1512step2 line 120
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1512 line 122
  29. def OAI.MUB6.Certificate.PairSemantics.raw1513 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw1513step0 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw1513step1 line 143
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1513 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw1514 line 158
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1514 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw1515 line 164
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1515 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw1516 line 170
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1516 line 172
  39. def OAI.MUB6.Certificate.PairSemantics.raw1517 line 176
  40. def OAI.MUB6.Certificate.PairSemantics.raw1517step0 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw1517step1 line 180
  42. def OAI.MUB6.Certificate.PairSemantics.raw1517step2 line 182
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1517 line 184
  44. def OAI.MUB6.Certificate.PairSemantics.raw1518 line 201
  45. def OAI.MUB6.Certificate.PairSemantics.raw1518step0 line 203
  46. def OAI.MUB6.Certificate.PairSemantics.raw1518step1 line 205
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1518 line 207
  48. def OAI.MUB6.Certificate.PairSemantics.raw1519 line 220
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1519 line 222
  50. def OAI.MUB6.Certificate.PairSemantics.raw1520 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw1520step0 line 228
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1520 line 230
  53. def OAI.MUB6.Certificate.PairSemantics.raw1521 line 239
  54. def OAI.MUB6.Certificate.PairSemantics.raw1521step0 line 241
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1521 line 243
  56. def OAI.MUB6.Certificate.PairSemantics.raw1522 line 252
  57. def OAI.MUB6.Certificate.PairSemantics.raw1522step0 line 254
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1522 line 256
  59. def OAI.MUB6.Certificate.PairSemantics.raw1523 line 265
  60. def OAI.MUB6.Certificate.PairSemantics.raw1523step0 line 267
  61. def OAI.MUB6.Certificate.PairSemantics.raw1523step1 line 269
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1523 line 271
  63. def OAI.MUB6.Certificate.PairSemantics.raw1524 line 284
  64. def OAI.MUB6.Certificate.PairSemantics.raw1524step0 line 286
  65. def OAI.MUB6.Certificate.PairSemantics.raw1524step1 line 288
  66. def OAI.MUB6.Certificate.PairSemantics.raw1524step2 line 290
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1524 line 292
  68. def OAI.MUB6.Certificate.PairSemantics.raw1525 line 310
  69. def OAI.MUB6.Certificate.PairSemantics.raw1525step0 line 312
  70. def OAI.MUB6.Certificate.PairSemantics.raw1525step1 line 314
  71. def OAI.MUB6.Certificate.PairSemantics.raw1525step2 line 316
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1525 line 318
  73. def OAI.MUB6.Certificate.PairSemantics.raw1526 line 336
  74. def OAI.MUB6.Certificate.PairSemantics.raw1526step0 line 338
  75. def OAI.MUB6.Certificate.PairSemantics.raw1526step1 line 340
  76. def OAI.MUB6.Certificate.PairSemantics.raw1526step2 line 342
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1526 line 344
  78. def OAI.MUB6.Certificate.PairSemantics.raw1527 line 362
  79. def OAI.MUB6.Certificate.PairSemantics.raw1527step0 line 364
  80. def OAI.MUB6.Certificate.PairSemantics.raw1527step1 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw1527step2 line 368
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1527 line 370
  83. def OAI.MUB6.Certificate.PairSemantics.raw1528 line 388
  84. def OAI.MUB6.Certificate.PairSemantics.raw1528step0 line 390
  85. def OAI.MUB6.Certificate.PairSemantics.raw1528step1 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw1528step2 line 394
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1528 line 396
  88. def OAI.MUB6.Certificate.PairSemantics.raw1529 line 414
  89. def OAI.MUB6.Certificate.PairSemantics.raw1529step0 line 416
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1529 line 418
  91. def OAI.MUB6.Certificate.PairSemantics.raw1530 line 427
  92. def OAI.MUB6.Certificate.PairSemantics.raw1530step0 line 429
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1530 line 431
  94. def OAI.MUB6.Certificate.PairSemantics.raw1531 line 440
  95. def OAI.MUB6.Certificate.PairSemantics.raw1531step0 line 442
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1531 line 444
  97. def OAI.MUB6.Certificate.PairSemantics.raw1532 line 453
  98. def OAI.MUB6.Certificate.PairSemantics.raw1532step0 line 455
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical1532 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw1533 line 466
  101. def OAI.MUB6.Certificate.PairSemantics.raw1533step0 line 468
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical1533 line 470
  103. def OAI.MUB6.Certificate.PairSemantics.raw1534 line 479
  104. def OAI.MUB6.Certificate.PairSemantics.raw1534step0 line 481
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical1534 line 483
  106. def OAI.MUB6.Certificate.PairSemantics.raw1535 line 492
  107. def OAI.MUB6.Certificate.PairSemantics.raw1535step0 line 494
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical1535 line 496