OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical230.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7360 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw7360step0 line 25
  3. def OAI.MUB6.Certificate.PairSemantics.raw7360step1 line 27
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7360 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw7361 line 42
  6. def OAI.MUB6.Certificate.PairSemantics.raw7361step0 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw7361step1 line 46
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7361 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw7362 line 61
  10. def OAI.MUB6.Certificate.PairSemantics.raw7362step0 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw7362step1 line 65
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7362 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw7363 line 80
  14. def OAI.MUB6.Certificate.PairSemantics.raw7363step0 line 82
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7363 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw7364 line 93
  17. def OAI.MUB6.Certificate.PairSemantics.raw7364step0 line 95
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical7364 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw7365 line 106
  20. def OAI.MUB6.Certificate.PairSemantics.raw7365step0 line 108
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7365 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw7366 line 119
  23. def OAI.MUB6.Certificate.PairSemantics.raw7366step0 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw7366step1 line 123
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7366 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw7367 line 138
  27. def OAI.MUB6.Certificate.PairSemantics.raw7367step0 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw7367step1 line 142
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical7367 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw7368 line 157
  31. def OAI.MUB6.Certificate.PairSemantics.raw7368step0 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw7368step1 line 161
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7368 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw7369 line 176
  35. def OAI.MUB6.Certificate.PairSemantics.raw7369step0 line 178
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7369 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw7370 line 189
  38. def OAI.MUB6.Certificate.PairSemantics.raw7370step0 line 191
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7370 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw7371 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw7371step0 line 204
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7371 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw7372 line 215
  44. def OAI.MUB6.Certificate.PairSemantics.raw7372step0 line 217
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7372 line 219
  46. def OAI.MUB6.Certificate.PairSemantics.raw7373 line 228
  47. def OAI.MUB6.Certificate.PairSemantics.raw7373step0 line 230
  48. def OAI.MUB6.Certificate.PairSemantics.raw7373step1 line 232
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical7373 line 234
  50. def OAI.MUB6.Certificate.PairSemantics.raw7374 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw7374step0 line 249
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7374 line 251
  53. def OAI.MUB6.Certificate.PairSemantics.raw7375 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw7375step0 line 262
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7375 line 264
  56. def OAI.MUB6.Certificate.PairSemantics.raw7376 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw7376step0 line 275
  58. def OAI.MUB6.Certificate.PairSemantics.raw7376step1 line 277
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7376 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw7377 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw7377step0 line 294
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7377 line 296
  63. def OAI.MUB6.Certificate.PairSemantics.raw7378 line 305
  64. def OAI.MUB6.Certificate.PairSemantics.raw7378step0 line 307
  65. def OAI.MUB6.Certificate.PairSemantics.raw7378step1 line 309
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7378 line 311
  67. def OAI.MUB6.Certificate.PairSemantics.raw7379 line 324
  68. def OAI.MUB6.Certificate.PairSemantics.raw7379step0 line 326
  69. def OAI.MUB6.Certificate.PairSemantics.raw7379step1 line 328
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7379 line 330
  71. def OAI.MUB6.Certificate.PairSemantics.raw7380 line 343
  72. def OAI.MUB6.Certificate.PairSemantics.raw7380step0 line 345
  73. def OAI.MUB6.Certificate.PairSemantics.raw7380step1 line 347
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7380 line 349
  75. def OAI.MUB6.Certificate.PairSemantics.raw7381 line 362
  76. def OAI.MUB6.Certificate.PairSemantics.raw7381step0 line 364
  77. def OAI.MUB6.Certificate.PairSemantics.raw7381step1 line 366
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7381 line 368
  79. def OAI.MUB6.Certificate.PairSemantics.raw7382 line 381
  80. def OAI.MUB6.Certificate.PairSemantics.raw7382step0 line 383
  81. def OAI.MUB6.Certificate.PairSemantics.raw7382step1 line 385
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7382 line 387
  83. def OAI.MUB6.Certificate.PairSemantics.raw7383 line 400
  84. def OAI.MUB6.Certificate.PairSemantics.raw7383step0 line 402
  85. def OAI.MUB6.Certificate.PairSemantics.raw7383step1 line 404
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical7383 line 406
  87. def OAI.MUB6.Certificate.PairSemantics.raw7384 line 419
  88. def OAI.MUB6.Certificate.PairSemantics.raw7384step0 line 421
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7384 line 423
  90. def OAI.MUB6.Certificate.PairSemantics.raw7385 line 432
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7385 line 434
  92. def OAI.MUB6.Certificate.PairSemantics.raw7386 line 438
  93. def OAI.MUB6.Certificate.PairSemantics.raw7386step0 line 440
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7386 line 442
  95. def OAI.MUB6.Certificate.PairSemantics.raw7387 line 451
  96. def OAI.MUB6.Certificate.PairSemantics.raw7387step0 line 453
  97. def OAI.MUB6.Certificate.PairSemantics.raw7387step1 line 455
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7387 line 457
  99. def OAI.MUB6.Certificate.PairSemantics.raw7388 line 470
  100. def OAI.MUB6.Certificate.PairSemantics.raw7388step0 line 472
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7388 line 474
  102. def OAI.MUB6.Certificate.PairSemantics.raw7389 line 483
  103. def OAI.MUB6.Certificate.PairSemantics.raw7389step0 line 485
  104. def OAI.MUB6.Certificate.PairSemantics.raw7389step1 line 487
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7389 line 489
  106. def OAI.MUB6.Certificate.PairSemantics.raw7390 line 502
  107. def OAI.MUB6.Certificate.PairSemantics.raw7390step0 line 504
  108. def OAI.MUB6.Certificate.PairSemantics.raw7390step1 line 506
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical7390 line 508
  110. def OAI.MUB6.Certificate.PairSemantics.raw7391 line 521
  111. def OAI.MUB6.Certificate.PairSemantics.raw7391step0 line 523
  112. def OAI.MUB6.Certificate.PairSemantics.raw7391step1 line 525
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7391 line 527