OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical295.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9440 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw9440step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9440 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw9441 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw9441step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9441 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw9442 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw9442step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9442 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw9443 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw9443step0 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9443 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw9444 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw9444step0 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9444 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw9445 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw9445step0 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw9445step1 line 84
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9445 line 86
  20. def OAI.MUB6.Certificate.PairSemantics.raw9446 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw9446step0 line 101
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9446 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw9447 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw9447step0 line 114
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9447 line 116
  26. def OAI.MUB6.Certificate.PairSemantics.raw9448 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw9448step0 line 127
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9448 line 129
  29. def OAI.MUB6.Certificate.PairSemantics.raw9449 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw9449step0 line 140
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9449 line 142
  32. def OAI.MUB6.Certificate.PairSemantics.raw9450 line 151
  33. def OAI.MUB6.Certificate.PairSemantics.raw9450step0 line 153
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9450 line 155
  35. def OAI.MUB6.Certificate.PairSemantics.raw9451 line 164
  36. def OAI.MUB6.Certificate.PairSemantics.raw9451step0 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw9451step1 line 168
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9451 line 170
  39. def OAI.MUB6.Certificate.PairSemantics.raw9452 line 184
  40. def OAI.MUB6.Certificate.PairSemantics.raw9452step0 line 186
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9452 line 188
  42. def OAI.MUB6.Certificate.PairSemantics.raw9453 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw9453step0 line 199
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9453 line 201
  45. def OAI.MUB6.Certificate.PairSemantics.raw9454 line 210
  46. def OAI.MUB6.Certificate.PairSemantics.raw9454step0 line 212
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9454 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw9455 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw9455step0 line 225
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9455 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw9456 line 236
  52. def OAI.MUB6.Certificate.PairSemantics.raw9456step0 line 238
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9456 line 240
  54. def OAI.MUB6.Certificate.PairSemantics.raw9457 line 249
  55. def OAI.MUB6.Certificate.PairSemantics.raw9457step0 line 251
  56. def OAI.MUB6.Certificate.PairSemantics.raw9457step1 line 253
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9457 line 255
  58. def OAI.MUB6.Certificate.PairSemantics.raw9458 line 268
  59. def OAI.MUB6.Certificate.PairSemantics.raw9458step0 line 270
  60. def OAI.MUB6.Certificate.PairSemantics.raw9458step1 line 272
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9458 line 274
  62. def OAI.MUB6.Certificate.PairSemantics.raw9459 line 287
  63. def OAI.MUB6.Certificate.PairSemantics.raw9459step0 line 289
  64. def OAI.MUB6.Certificate.PairSemantics.raw9459step1 line 291
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9459 line 293
  66. def OAI.MUB6.Certificate.PairSemantics.raw9460 line 306
  67. def OAI.MUB6.Certificate.PairSemantics.raw9460step0 line 308
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9460 line 310
  69. def OAI.MUB6.Certificate.PairSemantics.raw9461 line 319
  70. def OAI.MUB6.Certificate.PairSemantics.raw9461step0 line 321
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9461 line 323
  72. def OAI.MUB6.Certificate.PairSemantics.raw9462 line 332
  73. def OAI.MUB6.Certificate.PairSemantics.raw9462step0 line 334
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9462 line 336
  75. def OAI.MUB6.Certificate.PairSemantics.raw9463 line 345
  76. def OAI.MUB6.Certificate.PairSemantics.raw9463step0 line 347
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9463 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw9464 line 358
  79. def OAI.MUB6.Certificate.PairSemantics.raw9464step0 line 360
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical9464 line 362
  81. def OAI.MUB6.Certificate.PairSemantics.raw9465 line 371
  82. def OAI.MUB6.Certificate.PairSemantics.raw9465step0 line 373
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9465 line 375
  84. def OAI.MUB6.Certificate.PairSemantics.raw9466 line 384
  85. def OAI.MUB6.Certificate.PairSemantics.raw9466step0 line 386
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9466 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw9467 line 397
  88. def OAI.MUB6.Certificate.PairSemantics.raw9467step0 line 399
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9467 line 401
  90. def OAI.MUB6.Certificate.PairSemantics.raw9468 line 410
  91. def OAI.MUB6.Certificate.PairSemantics.raw9468step0 line 412
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9468 line 414
  93. def OAI.MUB6.Certificate.PairSemantics.raw9469 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw9469step0 line 425
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9469 line 427
  96. def OAI.MUB6.Certificate.PairSemantics.raw9470 line 436
  97. def OAI.MUB6.Certificate.PairSemantics.raw9470step0 line 438
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9470 line 440
  99. def OAI.MUB6.Certificate.PairSemantics.raw9471 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw9471step0 line 451
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical9471 line 453