OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical12.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw384 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw384step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw384step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical384 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw385 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw385step0 line 43
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical385 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw386 line 54
  9. def OAI.MUB6.Certificate.PairSemantics.raw386step0 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw386step1 line 58
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical386 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw387 line 73
  13. def OAI.MUB6.Certificate.PairSemantics.raw387step0 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw387step1 line 77
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical387 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw388 line 92
  17. def OAI.MUB6.Certificate.PairSemantics.raw388step0 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw388step1 line 96
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical388 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw389 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw389step0 line 113
  22. def OAI.MUB6.Certificate.PairSemantics.raw389step1 line 115
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical389 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw390 line 130
  25. def OAI.MUB6.Certificate.PairSemantics.raw390step0 line 132
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical390 line 134
  27. def OAI.MUB6.Certificate.PairSemantics.raw391 line 143
  28. def OAI.MUB6.Certificate.PairSemantics.raw391step0 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw391step1 line 147
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical391 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw392 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw392step0 line 164
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical392 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw393 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw393step0 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw393step1 line 179
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical393 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw394 line 194
  39. def OAI.MUB6.Certificate.PairSemantics.raw394step0 line 196
  40. def OAI.MUB6.Certificate.PairSemantics.raw394step1 line 198
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical394 line 200
  42. def OAI.MUB6.Certificate.PairSemantics.raw395 line 213
  43. def OAI.MUB6.Certificate.PairSemantics.raw395step0 line 215
  44. def OAI.MUB6.Certificate.PairSemantics.raw395step1 line 217
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical395 line 219
  46. def OAI.MUB6.Certificate.PairSemantics.raw396 line 232
  47. def OAI.MUB6.Certificate.PairSemantics.raw396step0 line 234
  48. def OAI.MUB6.Certificate.PairSemantics.raw396step1 line 236
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical396 line 238
  50. def OAI.MUB6.Certificate.PairSemantics.raw397 line 251
  51. def OAI.MUB6.Certificate.PairSemantics.raw397step0 line 253
  52. def OAI.MUB6.Certificate.PairSemantics.raw397step1 line 255
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical397 line 257
  54. def OAI.MUB6.Certificate.PairSemantics.raw398 line 270
  55. def OAI.MUB6.Certificate.PairSemantics.raw398step0 line 272
  56. def OAI.MUB6.Certificate.PairSemantics.raw398step1 line 274
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical398 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw399 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw399step0 line 291
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical399 line 293
  61. def OAI.MUB6.Certificate.PairSemantics.raw400 line 302
  62. def OAI.MUB6.Certificate.PairSemantics.raw400step0 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw400step1 line 306
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical400 line 308
  65. def OAI.MUB6.Certificate.PairSemantics.raw401 line 321
  66. def OAI.MUB6.Certificate.PairSemantics.raw401step0 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw401step1 line 325
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical401 line 327
  69. def OAI.MUB6.Certificate.PairSemantics.raw402 line 340
  70. def OAI.MUB6.Certificate.PairSemantics.raw402step0 line 342
  71. def OAI.MUB6.Certificate.PairSemantics.raw402step1 line 344
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical402 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw403 line 359
  74. def OAI.MUB6.Certificate.PairSemantics.raw403step0 line 361
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical403 line 363
  76. def OAI.MUB6.Certificate.PairSemantics.raw404 line 372
  77. def OAI.MUB6.Certificate.PairSemantics.raw404step0 line 374
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical404 line 376
  79. def OAI.MUB6.Certificate.PairSemantics.raw405 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw405step0 line 387
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical405 line 389
  82. def OAI.MUB6.Certificate.PairSemantics.raw406 line 398
  83. def OAI.MUB6.Certificate.PairSemantics.raw406step0 line 400
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical406 line 402
  85. def OAI.MUB6.Certificate.PairSemantics.raw407 line 411
  86. def OAI.MUB6.Certificate.PairSemantics.raw407step0 line 413
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical407 line 415
  88. def OAI.MUB6.Certificate.PairSemantics.raw408 line 424
  89. def OAI.MUB6.Certificate.PairSemantics.raw408step0 line 426
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical408 line 428
  91. def OAI.MUB6.Certificate.PairSemantics.raw409 line 437
  92. def OAI.MUB6.Certificate.PairSemantics.raw409step0 line 439
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical409 line 441
  94. def OAI.MUB6.Certificate.PairSemantics.raw410 line 450
  95. def OAI.MUB6.Certificate.PairSemantics.raw410step0 line 452
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical410 line 454
  97. def OAI.MUB6.Certificate.PairSemantics.raw411 line 463
  98. def OAI.MUB6.Certificate.PairSemantics.raw411step0 line 465
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical411 line 467
  100. def OAI.MUB6.Certificate.PairSemantics.raw412 line 476
  101. def OAI.MUB6.Certificate.PairSemantics.raw412step0 line 478
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical412 line 480
  103. def OAI.MUB6.Certificate.PairSemantics.raw413 line 489
  104. def OAI.MUB6.Certificate.PairSemantics.raw413step0 line 491
  105. def OAI.MUB6.Certificate.PairSemantics.raw413step1 line 493
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical413 line 495
  107. def OAI.MUB6.Certificate.PairSemantics.raw414 line 508
  108. def OAI.MUB6.Certificate.PairSemantics.raw414step0 line 510
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical414 line 512
  110. def OAI.MUB6.Certificate.PairSemantics.raw415 line 521
  111. def OAI.MUB6.Certificate.PairSemantics.raw415step0 line 523
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical415 line 525