OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical190.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6080 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw6080step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw6080step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6080 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw6081 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw6081step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw6081step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6081 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw6082 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw6082step0 line 59
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6082 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw6083 line 70
  13. def OAI.MUB6.Certificate.PairSemantics.raw6083step0 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw6083step1 line 74
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6083 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw6084 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw6084step0 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw6084step1 line 93
  19. def OAI.MUB6.Certificate.PairSemantics.raw6084step2 line 95
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6084 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw6085 line 115
  22. def OAI.MUB6.Certificate.PairSemantics.raw6085step0 line 117
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical6085 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw6086 line 128
  25. def OAI.MUB6.Certificate.PairSemantics.raw6086step0 line 130
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6086 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw6087 line 141
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6087 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw6088 line 147
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6088 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw6089 line 153
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6089 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw6090 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw6090step0 line 161
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6090 line 163
  36. def OAI.MUB6.Certificate.PairSemantics.raw6091 line 172
  37. def OAI.MUB6.Certificate.PairSemantics.raw6091step0 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw6091step1 line 176
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6091 line 178
  40. def OAI.MUB6.Certificate.PairSemantics.raw6092 line 191
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6092 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw6093 line 197
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6093 line 199
  44. def OAI.MUB6.Certificate.PairSemantics.raw6094 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw6094step0 line 205
  46. def OAI.MUB6.Certificate.PairSemantics.raw6094step1 line 207
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6094 line 209
  48. def OAI.MUB6.Certificate.PairSemantics.raw6095 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw6095step0 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw6095step1 line 226
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6095 line 228
  52. def OAI.MUB6.Certificate.PairSemantics.raw6096 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw6096step0 line 243
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6096 line 245
  55. def OAI.MUB6.Certificate.PairSemantics.raw6097 line 254
  56. def OAI.MUB6.Certificate.PairSemantics.raw6097step0 line 256
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6097 line 258
  58. def OAI.MUB6.Certificate.PairSemantics.raw6098 line 267
  59. def OAI.MUB6.Certificate.PairSemantics.raw6098step0 line 269
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6098 line 271
  61. def OAI.MUB6.Certificate.PairSemantics.raw6099 line 280
  62. def OAI.MUB6.Certificate.PairSemantics.raw6099step0 line 282
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6099 line 284
  64. def OAI.MUB6.Certificate.PairSemantics.raw6100 line 293
  65. def OAI.MUB6.Certificate.PairSemantics.raw6100step0 line 295
  66. def OAI.MUB6.Certificate.PairSemantics.raw6100step1 line 297
  67. def OAI.MUB6.Certificate.PairSemantics.raw6100step2 line 299
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6100 line 301
  69. def OAI.MUB6.Certificate.PairSemantics.raw6101 line 318
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6101 line 320
  71. def OAI.MUB6.Certificate.PairSemantics.raw6102 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw6102step0 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw6102step1 line 328
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6102 line 330
  75. def OAI.MUB6.Certificate.PairSemantics.raw6103 line 343
  76. def OAI.MUB6.Certificate.PairSemantics.raw6103step0 line 345
  77. def OAI.MUB6.Certificate.PairSemantics.raw6103step1 line 347
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6103 line 349
  79. def OAI.MUB6.Certificate.PairSemantics.raw6104 line 362
  80. def OAI.MUB6.Certificate.PairSemantics.raw6104step0 line 364
  81. def OAI.MUB6.Certificate.PairSemantics.raw6104step1 line 366
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6104 line 368
  83. def OAI.MUB6.Certificate.PairSemantics.raw6105 line 381
  84. def OAI.MUB6.Certificate.PairSemantics.raw6105step0 line 383
  85. def OAI.MUB6.Certificate.PairSemantics.raw6105step1 line 385
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6105 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw6106 line 400
  88. def OAI.MUB6.Certificate.PairSemantics.raw6106step0 line 402
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6106 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw6107 line 413
  91. def OAI.MUB6.Certificate.PairSemantics.raw6107step0 line 415
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical6107 line 417
  93. def OAI.MUB6.Certificate.PairSemantics.raw6108 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw6108step0 line 428
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6108 line 430
  96. def OAI.MUB6.Certificate.PairSemantics.raw6109 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw6109step0 line 441
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical6109 line 443
  99. def OAI.MUB6.Certificate.PairSemantics.raw6110 line 452
  100. def OAI.MUB6.Certificate.PairSemantics.raw6110step0 line 454
  101. def OAI.MUB6.Certificate.PairSemantics.raw6110step1 line 456
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical6110 line 458
  103. def OAI.MUB6.Certificate.PairSemantics.raw6111 line 471
  104. def OAI.MUB6.Certificate.PairSemantics.raw6111step0 line 473
  105. def OAI.MUB6.Certificate.PairSemantics.raw6111step1 line 475
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical6111 line 477