OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical121.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3872 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw3872step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical3872 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw3873 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw3873step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical3873 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw3874 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw3874step0 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3874 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw3875 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw3875step0 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw3875step1 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3875 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw3876 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw3876step0 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3876 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw3877 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw3877step0 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw3877step1 line 92
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3877 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw3878 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw3878step0 line 109
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical3878 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw3879 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw3879step0 line 122
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3879 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw3880 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw3880step0 line 135
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3880 line 137
  30. def OAI.MUB6.Certificate.PairSemantics.raw3881 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw3881step0 line 148
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3881 line 150
  33. def OAI.MUB6.Certificate.PairSemantics.raw3882 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw3882step0 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw3882step1 line 163
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3882 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw3883 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3883step0 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw3883step1 line 182
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3883 line 184
  41. def OAI.MUB6.Certificate.PairSemantics.raw3884 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw3884step0 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw3884step1 line 201
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical3884 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw3885 line 216
  46. def OAI.MUB6.Certificate.PairSemantics.raw3885step0 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw3885step1 line 220
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3885 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw3886 line 235
  50. def OAI.MUB6.Certificate.PairSemantics.raw3886step0 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw3886step1 line 239
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3886 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw3887 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw3887step0 line 256
  55. def OAI.MUB6.Certificate.PairSemantics.raw3887step1 line 258
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3887 line 260
  57. def OAI.MUB6.Certificate.PairSemantics.raw3888 line 273
  58. def OAI.MUB6.Certificate.PairSemantics.raw3888step0 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw3888step1 line 277
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical3888 line 279
  61. def OAI.MUB6.Certificate.PairSemantics.raw3889 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw3889step0 line 294
  63. def OAI.MUB6.Certificate.PairSemantics.raw3889step1 line 296
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3889 line 298
  65. def OAI.MUB6.Certificate.PairSemantics.raw3890 line 311
  66. def OAI.MUB6.Certificate.PairSemantics.raw3890step0 line 313
  67. def OAI.MUB6.Certificate.PairSemantics.raw3890step1 line 315
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3890 line 317
  69. def OAI.MUB6.Certificate.PairSemantics.raw3891 line 330
  70. def OAI.MUB6.Certificate.PairSemantics.raw3891step0 line 332
  71. def OAI.MUB6.Certificate.PairSemantics.raw3891step1 line 334
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3891 line 336
  73. def OAI.MUB6.Certificate.PairSemantics.raw3892 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw3892step0 line 351
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3892 line 353
  76. def OAI.MUB6.Certificate.PairSemantics.raw3893 line 362
  77. def OAI.MUB6.Certificate.PairSemantics.raw3893step0 line 364
  78. def OAI.MUB6.Certificate.PairSemantics.raw3893step1 line 366
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3893 line 368
  80. def OAI.MUB6.Certificate.PairSemantics.raw3894 line 381
  81. def OAI.MUB6.Certificate.PairSemantics.raw3894step0 line 383
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3894 line 385
  83. def OAI.MUB6.Certificate.PairSemantics.raw3895 line 394
  84. def OAI.MUB6.Certificate.PairSemantics.raw3895step0 line 396
  85. def OAI.MUB6.Certificate.PairSemantics.raw3895step1 line 398
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3895 line 400
  87. def OAI.MUB6.Certificate.PairSemantics.raw3896 line 413
  88. def OAI.MUB6.Certificate.PairSemantics.raw3896step0 line 415
  89. def OAI.MUB6.Certificate.PairSemantics.raw3896step1 line 417
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3896 line 419
  91. def OAI.MUB6.Certificate.PairSemantics.raw3897 line 432
  92. def OAI.MUB6.Certificate.PairSemantics.raw3897step0 line 434
  93. def OAI.MUB6.Certificate.PairSemantics.raw3897step1 line 436
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3897 line 438
  95. def OAI.MUB6.Certificate.PairSemantics.raw3898 line 451
  96. def OAI.MUB6.Certificate.PairSemantics.raw3898step0 line 453
  97. def OAI.MUB6.Certificate.PairSemantics.raw3898step1 line 455
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3898 line 457
  99. def OAI.MUB6.Certificate.PairSemantics.raw3899 line 470
  100. def OAI.MUB6.Certificate.PairSemantics.raw3899step0 line 472
  101. def OAI.MUB6.Certificate.PairSemantics.raw3899step1 line 474
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3899 line 476
  103. def OAI.MUB6.Certificate.PairSemantics.raw3900 line 489
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3900 line 491
  105. def OAI.MUB6.Certificate.PairSemantics.raw3901 line 495
  106. def OAI.MUB6.Certificate.PairSemantics.raw3901step0 line 497
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3901 line 499
  108. def OAI.MUB6.Certificate.PairSemantics.raw3902 line 508
  109. def OAI.MUB6.Certificate.PairSemantics.raw3902step0 line 510
  110. def OAI.MUB6.Certificate.PairSemantics.raw3902step1 line 512
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical3902 line 514
  112. def OAI.MUB6.Certificate.PairSemantics.raw3903 line 527
  113. def OAI.MUB6.Certificate.PairSemantics.raw3903step0 line 529
  114. def OAI.MUB6.Certificate.PairSemantics.raw3903step1 line 531
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical3903 line 533