OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical13.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw416 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw416step0 line 23
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical416 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw417 line 34
  5. def OAI.MUB6.Certificate.PairSemantics.raw417step0 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw417step1 line 38
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical417 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw418 line 53
  9. def OAI.MUB6.Certificate.PairSemantics.raw418step0 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw418step1 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical418 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw419 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw419step0 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw419step1 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical419 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw420 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw420step0 line 93
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical420 line 95
  19. def OAI.MUB6.Certificate.PairSemantics.raw421 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw421step0 line 106
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical421 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw422 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw422step0 line 119
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical422 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw423 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw423step0 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical423 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw424 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw424step0 line 145
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical424 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw425 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw425step0 line 158
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical425 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw426 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw426step0 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical426 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw427 line 182
  38. def OAI.MUB6.Certificate.PairSemantics.raw427step0 line 184
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical427 line 186
  40. def OAI.MUB6.Certificate.PairSemantics.raw428 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw428step0 line 197
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical428 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw429 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw429step0 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical429 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw430 line 221
  47. def OAI.MUB6.Certificate.PairSemantics.raw430step0 line 223
  48. def OAI.MUB6.Certificate.PairSemantics.raw430step1 line 225
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical430 line 227
  50. def OAI.MUB6.Certificate.PairSemantics.raw431 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw431step0 line 242
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical431 line 244
  53. def OAI.MUB6.Certificate.PairSemantics.raw432 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw432step0 line 255
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical432 line 257
  56. def OAI.MUB6.Certificate.PairSemantics.raw433 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw433step0 line 268
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical433 line 270
  59. def OAI.MUB6.Certificate.PairSemantics.raw434 line 279
  60. def OAI.MUB6.Certificate.PairSemantics.raw434step0 line 281
  61. def OAI.MUB6.Certificate.PairSemantics.raw434step1 line 283
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical434 line 285
  63. def OAI.MUB6.Certificate.PairSemantics.raw435 line 298
  64. def OAI.MUB6.Certificate.PairSemantics.raw435step0 line 300
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical435 line 302
  66. def OAI.MUB6.Certificate.PairSemantics.raw436 line 311
  67. def OAI.MUB6.Certificate.PairSemantics.raw436step0 line 313
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical436 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw437 line 324
  70. def OAI.MUB6.Certificate.PairSemantics.raw437step0 line 326
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical437 line 328
  72. def OAI.MUB6.Certificate.PairSemantics.raw438 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw438step0 line 339
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical438 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw439 line 350
  76. def OAI.MUB6.Certificate.PairSemantics.raw439step0 line 352
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical439 line 354
  78. def OAI.MUB6.Certificate.PairSemantics.raw440 line 363
  79. def OAI.MUB6.Certificate.PairSemantics.raw440step0 line 365
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical440 line 367
  81. def OAI.MUB6.Certificate.PairSemantics.raw441 line 376
  82. def OAI.MUB6.Certificate.PairSemantics.raw441step0 line 378
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical441 line 380
  84. def OAI.MUB6.Certificate.PairSemantics.raw442 line 389
  85. def OAI.MUB6.Certificate.PairSemantics.raw442step0 line 391
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical442 line 393
  87. def OAI.MUB6.Certificate.PairSemantics.raw443 line 402
  88. def OAI.MUB6.Certificate.PairSemantics.raw443step0 line 404
  89. def OAI.MUB6.Certificate.PairSemantics.raw443step1 line 406
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical443 line 408
  91. def OAI.MUB6.Certificate.PairSemantics.raw444 line 421
  92. def OAI.MUB6.Certificate.PairSemantics.raw444step0 line 423
  93. def OAI.MUB6.Certificate.PairSemantics.raw444step1 line 425
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical444 line 427
  95. def OAI.MUB6.Certificate.PairSemantics.raw445 line 440
  96. def OAI.MUB6.Certificate.PairSemantics.raw445step0 line 442
  97. def OAI.MUB6.Certificate.PairSemantics.raw445step1 line 444
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical445 line 446
  99. def OAI.MUB6.Certificate.PairSemantics.raw446 line 459
  100. def OAI.MUB6.Certificate.PairSemantics.raw446step0 line 461
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical446 line 463
  102. def OAI.MUB6.Certificate.PairSemantics.raw447 line 472
  103. def OAI.MUB6.Certificate.PairSemantics.raw447step0 line 474
  104. def OAI.MUB6.Certificate.PairSemantics.raw447step1 line 476
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical447 line 478