OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical162.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5184 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw5184step0 line 12
  3. def OAI.MUB6.Certificate.PairSemantics.raw5184step1 line 14
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5184 line 16
  5. def OAI.MUB6.Certificate.PairSemantics.raw5185 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw5185step0 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw5185step1 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5185 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw5186 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw5186step0 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw5186step1 line 55
  12. def OAI.MUB6.Certificate.PairSemantics.raw5186step2 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw5186step3 line 59
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5186 line 61
  15. def OAI.MUB6.Certificate.PairSemantics.raw5187 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw5187step0 line 88
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5187 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw5188 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw5188step0 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw5188step1 line 103
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5188 line 105
  22. def OAI.MUB6.Certificate.PairSemantics.raw5189 line 119
  23. def OAI.MUB6.Certificate.PairSemantics.raw5189step0 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw5189step1 line 123
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5189 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw5190 line 139
  27. def OAI.MUB6.Certificate.PairSemantics.raw5190step0 line 141
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5190 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw5191 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw5191step0 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw5191step1 line 156
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5191 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw5192 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw5192step0 line 174
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5192 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw5193 line 185
  37. def OAI.MUB6.Certificate.PairSemantics.raw5193step0 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw5193step1 line 189
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5193 line 191
  40. def OAI.MUB6.Certificate.PairSemantics.raw5194 line 205
  41. def OAI.MUB6.Certificate.PairSemantics.raw5194step0 line 207
  42. def OAI.MUB6.Certificate.PairSemantics.raw5194step1 line 209
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5194 line 211
  44. def OAI.MUB6.Certificate.PairSemantics.raw5195 line 225
  45. def OAI.MUB6.Certificate.PairSemantics.raw5195step0 line 227
  46. def OAI.MUB6.Certificate.PairSemantics.raw5195step1 line 229
  47. def OAI.MUB6.Certificate.PairSemantics.raw5195step2 line 231
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5195 line 233
  49. def OAI.MUB6.Certificate.PairSemantics.raw5196 line 253
  50. def OAI.MUB6.Certificate.PairSemantics.raw5196step0 line 255
  51. def OAI.MUB6.Certificate.PairSemantics.raw5196step1 line 257
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5196 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw5197 line 274
  54. def OAI.MUB6.Certificate.PairSemantics.raw5197step0 line 276
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5197 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw5198 line 288
  57. def OAI.MUB6.Certificate.PairSemantics.raw5198step0 line 290
  58. def OAI.MUB6.Certificate.PairSemantics.raw5198step1 line 292
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5198 line 294
  60. def OAI.MUB6.Certificate.PairSemantics.raw5199 line 309
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5199 line 311
  62. def OAI.MUB6.Certificate.PairSemantics.raw5200 line 315
  63. def OAI.MUB6.Certificate.PairSemantics.raw5200step0 line 317
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5200 line 319
  65. def OAI.MUB6.Certificate.PairSemantics.raw5201 line 328
  66. def OAI.MUB6.Certificate.PairSemantics.raw5201step0 line 330
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5201 line 332
  68. def OAI.MUB6.Certificate.PairSemantics.raw5202 line 341
  69. def OAI.MUB6.Certificate.PairSemantics.raw5202step0 line 343
  70. def OAI.MUB6.Certificate.PairSemantics.raw5202step1 line 345
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5202 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw5203 line 361
  73. def OAI.MUB6.Certificate.PairSemantics.raw5203step0 line 363
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5203 line 365
  75. def OAI.MUB6.Certificate.PairSemantics.raw5204 line 374
  76. def OAI.MUB6.Certificate.PairSemantics.raw5204step0 line 376
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5204 line 378
  78. def OAI.MUB6.Certificate.PairSemantics.raw5205 line 388
  79. def OAI.MUB6.Certificate.PairSemantics.raw5205step0 line 390
  80. def OAI.MUB6.Certificate.PairSemantics.raw5205step1 line 392
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5205 line 394
  82. def OAI.MUB6.Certificate.PairSemantics.raw5206 line 409
  83. def OAI.MUB6.Certificate.PairSemantics.raw5206step0 line 411
  84. def OAI.MUB6.Certificate.PairSemantics.raw5206step1 line 413
  85. def OAI.MUB6.Certificate.PairSemantics.raw5206step2 line 415
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical5206 line 417
  87. def OAI.MUB6.Certificate.PairSemantics.raw5207 line 437
  88. def OAI.MUB6.Certificate.PairSemantics.raw5207step0 line 439
  89. def OAI.MUB6.Certificate.PairSemantics.raw5207step1 line 441
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical5207 line 443
  91. def OAI.MUB6.Certificate.PairSemantics.raw5208 line 457
  92. def OAI.MUB6.Certificate.PairSemantics.raw5208step0 line 459
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5208 line 461
  94. def OAI.MUB6.Certificate.PairSemantics.raw5209 line 470
  95. def OAI.MUB6.Certificate.PairSemantics.raw5209step0 line 472
  96. def OAI.MUB6.Certificate.PairSemantics.raw5209step1 line 474
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical5209 line 476
  98. def OAI.MUB6.Certificate.PairSemantics.raw5210 line 490
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5210 line 492
  100. def OAI.MUB6.Certificate.PairSemantics.raw5211 line 496
  101. def OAI.MUB6.Certificate.PairSemantics.raw5211step0 line 498
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical5211 line 500
  103. def OAI.MUB6.Certificate.PairSemantics.raw5212 line 509
  104. def OAI.MUB6.Certificate.PairSemantics.raw5212step0 line 511
  105. def OAI.MUB6.Certificate.PairSemantics.raw5212step1 line 513
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical5212 line 515
  107. def OAI.MUB6.Certificate.PairSemantics.raw5213 line 529
  108. def OAI.MUB6.Certificate.PairSemantics.raw5213step0 line 531
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical5213 line 533
  110. def OAI.MUB6.Certificate.PairSemantics.raw5214 line 542
  111. def OAI.MUB6.Certificate.PairSemantics.raw5214step0 line 544
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical5214 line 546
  113. def OAI.MUB6.Certificate.PairSemantics.raw5215 line 556
  114. def OAI.MUB6.Certificate.PairSemantics.raw5215step0 line 558
  115. def OAI.MUB6.Certificate.PairSemantics.raw5215step1 line 560
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical5215 line 562