OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical197.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6304 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw6304step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw6304step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6304 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw6305 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw6305step0 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical6305 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw6306 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw6306step0 line 48
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6306 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw6307 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw6307step0 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6307 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw6308 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw6308step0 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw6308step1 line 76
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6308 line 78
  18. def OAI.MUB6.Certificate.PairSemantics.raw6309 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw6309step0 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw6309step1 line 95
  21. def OAI.MUB6.Certificate.PairSemantics.raw6309step2 line 97
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6309 line 99
  23. def OAI.MUB6.Certificate.PairSemantics.raw6310 line 116
  24. def OAI.MUB6.Certificate.PairSemantics.raw6310step0 line 118
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6310 line 120
  26. def OAI.MUB6.Certificate.PairSemantics.raw6311 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw6311step0 line 131
  28. def OAI.MUB6.Certificate.PairSemantics.raw6311step1 line 133
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6311 line 135
  30. def OAI.MUB6.Certificate.PairSemantics.raw6312 line 148
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6312 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw6313 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw6313step0 line 156
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6313 line 158
  35. def OAI.MUB6.Certificate.PairSemantics.raw6314 line 167
  36. def OAI.MUB6.Certificate.PairSemantics.raw6314step0 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw6314step1 line 171
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6314 line 173
  39. def OAI.MUB6.Certificate.PairSemantics.raw6315 line 186
  40. def OAI.MUB6.Certificate.PairSemantics.raw6315step0 line 188
  41. def OAI.MUB6.Certificate.PairSemantics.raw6315step1 line 190
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6315 line 192
  43. def OAI.MUB6.Certificate.PairSemantics.raw6316 line 205
  44. def OAI.MUB6.Certificate.PairSemantics.raw6316step0 line 207
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6316 line 209
  46. def OAI.MUB6.Certificate.PairSemantics.raw6317 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw6317step0 line 220
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6317 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw6318 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw6318step0 line 233
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6318 line 235
  52. def OAI.MUB6.Certificate.PairSemantics.raw6319 line 244
  53. def OAI.MUB6.Certificate.PairSemantics.raw6319step0 line 246
  54. def OAI.MUB6.Certificate.PairSemantics.raw6319step1 line 248
  55. def OAI.MUB6.Certificate.PairSemantics.raw6319step2 line 250
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6319 line 252
  57. def OAI.MUB6.Certificate.PairSemantics.raw6320 line 269
  58. def OAI.MUB6.Certificate.PairSemantics.raw6320step0 line 271
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6320 line 273
  60. def OAI.MUB6.Certificate.PairSemantics.raw6321 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw6321step0 line 284
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6321 line 286
  63. def OAI.MUB6.Certificate.PairSemantics.raw6322 line 295
  64. def OAI.MUB6.Certificate.PairSemantics.raw6322step0 line 297
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6322 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw6323 line 308
  67. def OAI.MUB6.Certificate.PairSemantics.raw6323step0 line 310
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6323 line 312
  69. def OAI.MUB6.Certificate.PairSemantics.raw6324 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw6324step0 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw6324step1 line 325
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6324 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw6325 line 340
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6325 line 342
  75. def OAI.MUB6.Certificate.PairSemantics.raw6326 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw6326step0 line 348
  77. def OAI.MUB6.Certificate.PairSemantics.raw6326step1 line 350
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6326 line 352
  79. def OAI.MUB6.Certificate.PairSemantics.raw6327 line 365
  80. def OAI.MUB6.Certificate.PairSemantics.raw6327step0 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw6327step1 line 369
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6327 line 371
  83. def OAI.MUB6.Certificate.PairSemantics.raw6328 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw6328step0 line 386
  85. def OAI.MUB6.Certificate.PairSemantics.raw6328step1 line 388
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6328 line 390
  87. def OAI.MUB6.Certificate.PairSemantics.raw6329 line 403
  88. def OAI.MUB6.Certificate.PairSemantics.raw6329step0 line 405
  89. def OAI.MUB6.Certificate.PairSemantics.raw6329step1 line 407
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6329 line 409
  91. def OAI.MUB6.Certificate.PairSemantics.raw6330 line 422
  92. def OAI.MUB6.Certificate.PairSemantics.raw6330step0 line 424
  93. def OAI.MUB6.Certificate.PairSemantics.raw6330step1 line 426
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical6330 line 428
  95. def OAI.MUB6.Certificate.PairSemantics.raw6331 line 441
  96. def OAI.MUB6.Certificate.PairSemantics.raw6331step0 line 443
  97. def OAI.MUB6.Certificate.PairSemantics.raw6331step1 line 445
  98. def OAI.MUB6.Certificate.PairSemantics.raw6331step2 line 447
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6331 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw6332 line 466
  101. def OAI.MUB6.Certificate.PairSemantics.raw6332step0 line 468
  102. def OAI.MUB6.Certificate.PairSemantics.raw6332step1 line 470
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6332 line 472
  104. def OAI.MUB6.Certificate.PairSemantics.raw6333 line 485
  105. def OAI.MUB6.Certificate.PairSemantics.raw6333step0 line 487
  106. def OAI.MUB6.Certificate.PairSemantics.raw6333step1 line 489
  107. def OAI.MUB6.Certificate.PairSemantics.raw6333step2 line 491
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6333 line 493
  109. def OAI.MUB6.Certificate.PairSemantics.raw6334 line 510
  110. def OAI.MUB6.Certificate.PairSemantics.raw6334step0 line 512
  111. def OAI.MUB6.Certificate.PairSemantics.raw6334step1 line 514
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical6334 line 516
  113. def OAI.MUB6.Certificate.PairSemantics.raw6335 line 529
  114. def OAI.MUB6.Certificate.PairSemantics.raw6335step0 line 531
  115. def OAI.MUB6.Certificate.PairSemantics.raw6335step1 line 533
  116. def OAI.MUB6.Certificate.PairSemantics.raw6335step2 line 535
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical6335 line 537