OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical10.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw320 line 11
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical320 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw321 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw321step0 line 19
  5. def OAI.MUB6.Certificate.PairSemantics.raw321step1 line 21
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical321 line 23
  7. def OAI.MUB6.Certificate.PairSemantics.raw322 line 36
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical322 line 38
  9. def OAI.MUB6.Certificate.PairSemantics.raw323 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw323step0 line 44
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical323 line 46
  12. def OAI.MUB6.Certificate.PairSemantics.raw324 line 55
  13. def OAI.MUB6.Certificate.PairSemantics.raw324step0 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw324step1 line 59
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical324 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw325 line 74
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical325 line 76
  18. def OAI.MUB6.Certificate.PairSemantics.raw326 line 80
  19. def OAI.MUB6.Certificate.PairSemantics.raw326step0 line 82
  20. def OAI.MUB6.Certificate.PairSemantics.raw326step1 line 84
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical326 line 86
  22. def OAI.MUB6.Certificate.PairSemantics.raw327 line 99
  23. def OAI.MUB6.Certificate.PairSemantics.raw327step0 line 101
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical327 line 103
  25. def OAI.MUB6.Certificate.PairSemantics.raw328 line 112
  26. def OAI.MUB6.Certificate.PairSemantics.raw328step0 line 114
  27. def OAI.MUB6.Certificate.PairSemantics.raw328step1 line 116
  28. def OAI.MUB6.Certificate.PairSemantics.raw328step2 line 118
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical328 line 120
  30. def OAI.MUB6.Certificate.PairSemantics.raw329 line 137
  31. def OAI.MUB6.Certificate.PairSemantics.raw329step0 line 139
  32. def OAI.MUB6.Certificate.PairSemantics.raw329step1 line 141
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical329 line 143
  34. def OAI.MUB6.Certificate.PairSemantics.raw330 line 156
  35. def OAI.MUB6.Certificate.PairSemantics.raw330step0 line 158
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical330 line 160
  37. def OAI.MUB6.Certificate.PairSemantics.raw331 line 169
  38. def OAI.MUB6.Certificate.PairSemantics.raw331step0 line 171
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical331 line 173
  40. def OAI.MUB6.Certificate.PairSemantics.raw332 line 182
  41. def OAI.MUB6.Certificate.PairSemantics.raw332step0 line 184
  42. def OAI.MUB6.Certificate.PairSemantics.raw332step1 line 186
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical332 line 188
  44. def OAI.MUB6.Certificate.PairSemantics.raw333 line 201
  45. def OAI.MUB6.Certificate.PairSemantics.raw333step0 line 203
  46. def OAI.MUB6.Certificate.PairSemantics.raw333step1 line 205
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical333 line 207
  48. def OAI.MUB6.Certificate.PairSemantics.raw334 line 220
  49. def OAI.MUB6.Certificate.PairSemantics.raw334step0 line 222
  50. def OAI.MUB6.Certificate.PairSemantics.raw334step1 line 224
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical334 line 226
  52. def OAI.MUB6.Certificate.PairSemantics.raw335 line 239
  53. def OAI.MUB6.Certificate.PairSemantics.raw335step0 line 241
  54. def OAI.MUB6.Certificate.PairSemantics.raw335step1 line 243
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical335 line 245
  56. def OAI.MUB6.Certificate.PairSemantics.raw336 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw336step0 line 260
  58. def OAI.MUB6.Certificate.PairSemantics.raw336step1 line 262
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical336 line 264
  60. def OAI.MUB6.Certificate.PairSemantics.raw337 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw337step0 line 279
  62. def OAI.MUB6.Certificate.PairSemantics.raw337step1 line 281
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical337 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw338 line 296
  65. def OAI.MUB6.Certificate.PairSemantics.raw338step0 line 298
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical338 line 300
  67. def OAI.MUB6.Certificate.PairSemantics.raw339 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw339step0 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical339 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw340 line 322
  71. def OAI.MUB6.Certificate.PairSemantics.raw340step0 line 324
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical340 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw341 line 335
  74. def OAI.MUB6.Certificate.PairSemantics.raw341step0 line 337
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical341 line 339
  76. def OAI.MUB6.Certificate.PairSemantics.raw342 line 348
  77. def OAI.MUB6.Certificate.PairSemantics.raw342step0 line 350
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical342 line 352
  79. def OAI.MUB6.Certificate.PairSemantics.raw343 line 361
  80. def OAI.MUB6.Certificate.PairSemantics.raw343step0 line 363
  81. def OAI.MUB6.Certificate.PairSemantics.raw343step1 line 365
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical343 line 367
  83. def OAI.MUB6.Certificate.PairSemantics.raw344 line 380
  84. def OAI.MUB6.Certificate.PairSemantics.raw344step0 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw344step1 line 384
  86. def OAI.MUB6.Certificate.PairSemantics.raw344step2 line 386
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical344 line 388
  88. def OAI.MUB6.Certificate.PairSemantics.raw345 line 405
  89. def OAI.MUB6.Certificate.PairSemantics.raw345step0 line 407
  90. def OAI.MUB6.Certificate.PairSemantics.raw345step1 line 409
  91. def OAI.MUB6.Certificate.PairSemantics.raw345step2 line 411
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical345 line 413
  93. def OAI.MUB6.Certificate.PairSemantics.raw346 line 430
  94. def OAI.MUB6.Certificate.PairSemantics.raw346step0 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw346step1 line 434
  96. def OAI.MUB6.Certificate.PairSemantics.raw346step2 line 436
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical346 line 438
  98. def OAI.MUB6.Certificate.PairSemantics.raw347 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw347step0 line 457
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical347 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw348 line 468
  102. def OAI.MUB6.Certificate.PairSemantics.raw348step0 line 470
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical348 line 472
  104. def OAI.MUB6.Certificate.PairSemantics.raw349 line 481
  105. def OAI.MUB6.Certificate.PairSemantics.raw349step0 line 483
  106. def OAI.MUB6.Certificate.PairSemantics.raw349step1 line 485
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical349 line 487
  108. def OAI.MUB6.Certificate.PairSemantics.raw350 line 500
  109. def OAI.MUB6.Certificate.PairSemantics.raw350step0 line 502
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical350 line 504
  111. def OAI.MUB6.Certificate.PairSemantics.raw351 line 513
  112. def OAI.MUB6.Certificate.PairSemantics.raw351step0 line 515
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical351 line 517