OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical111.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3552 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw3552step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw3552step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3552 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw3553 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw3553step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw3553step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3553 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw3554 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw3554step0 line 61
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3554 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw3555 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw3555step0 line 74
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3555 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw3556 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw3556step0 line 87
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3556 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw3557 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw3557step0 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3557 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw3558 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw3558step0 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw3558step1 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3558 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw3559 line 130
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3559 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw3560 line 136
  28. def OAI.MUB6.Certificate.PairSemantics.raw3560step0 line 138
  29. def OAI.MUB6.Certificate.PairSemantics.raw3560step1 line 140
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3560 line 142
  31. def OAI.MUB6.Certificate.PairSemantics.raw3561 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw3561step0 line 157
  33. def OAI.MUB6.Certificate.PairSemantics.raw3561step1 line 159
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3561 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw3562 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw3562step0 line 176
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3562 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3563 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw3563step0 line 189
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3563 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw3564 line 200
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3564 line 202
  43. def OAI.MUB6.Certificate.PairSemantics.raw3565 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw3565step0 line 208
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3565 line 210
  46. def OAI.MUB6.Certificate.PairSemantics.raw3566 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw3566step0 line 221
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3566 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw3567 line 232
  50. def OAI.MUB6.Certificate.PairSemantics.raw3567step0 line 234
  51. def OAI.MUB6.Certificate.PairSemantics.raw3567step1 line 236
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3567 line 238
  53. def OAI.MUB6.Certificate.PairSemantics.raw3568 line 251
  54. def OAI.MUB6.Certificate.PairSemantics.raw3568step0 line 253
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3568 line 255
  56. def OAI.MUB6.Certificate.PairSemantics.raw3569 line 264
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3569 line 266
  58. def OAI.MUB6.Certificate.PairSemantics.raw3570 line 270
  59. def OAI.MUB6.Certificate.PairSemantics.raw3570step0 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw3570step1 line 274
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3570 line 276
  62. def OAI.MUB6.Certificate.PairSemantics.raw3571 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw3571step0 line 291
  64. def OAI.MUB6.Certificate.PairSemantics.raw3571step1 line 293
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3571 line 295
  66. def OAI.MUB6.Certificate.PairSemantics.raw3572 line 308
  67. def OAI.MUB6.Certificate.PairSemantics.raw3572step0 line 310
  68. def OAI.MUB6.Certificate.PairSemantics.raw3572step1 line 312
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3572 line 314
  70. def OAI.MUB6.Certificate.PairSemantics.raw3573 line 327
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical3573 line 329
  72. def OAI.MUB6.Certificate.PairSemantics.raw3574 line 333
  73. def OAI.MUB6.Certificate.PairSemantics.raw3574step0 line 335
  74. def OAI.MUB6.Certificate.PairSemantics.raw3574step1 line 337
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3574 line 339
  76. def OAI.MUB6.Certificate.PairSemantics.raw3575 line 352
  77. def OAI.MUB6.Certificate.PairSemantics.raw3575step0 line 354
  78. def OAI.MUB6.Certificate.PairSemantics.raw3575step1 line 356
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3575 line 358
  80. def OAI.MUB6.Certificate.PairSemantics.raw3576 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw3576step0 line 373
  82. def OAI.MUB6.Certificate.PairSemantics.raw3576step1 line 375
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3576 line 377
  84. def OAI.MUB6.Certificate.PairSemantics.raw3577 line 390
  85. def OAI.MUB6.Certificate.PairSemantics.raw3577step0 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw3577step1 line 394
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3577 line 396
  88. def OAI.MUB6.Certificate.PairSemantics.raw3578 line 409
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3578 line 411
  90. def OAI.MUB6.Certificate.PairSemantics.raw3579 line 415
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3579 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw3580 line 421
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3580 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw3581 line 427
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical3581 line 429
  96. def OAI.MUB6.Certificate.PairSemantics.raw3582 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw3582step0 line 435
  98. def OAI.MUB6.Certificate.PairSemantics.raw3582step1 line 437
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3582 line 439
  100. def OAI.MUB6.Certificate.PairSemantics.raw3583 line 452
  101. def OAI.MUB6.Certificate.PairSemantics.raw3583step0 line 454
  102. def OAI.MUB6.Certificate.PairSemantics.raw3583step1 line 456
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3583 line 458