OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical187.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5984 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw5984step0 line 25
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5984 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw5985 line 36
  5. def OAI.MUB6.Certificate.PairSemantics.raw5985step0 line 38
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5985 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw5986 line 49
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5986 line 51
  9. def OAI.MUB6.Certificate.PairSemantics.raw5987 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw5987step0 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5987 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw5988 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw5988step0 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5988 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw5989 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw5989step0 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5989 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw5990 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw5990step0 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw5990step1 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5990 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw5991 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw5991step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw5991step1 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw5991step2 line 119
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5991 line 121
  27. def OAI.MUB6.Certificate.PairSemantics.raw5992 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw5992step0 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw5992step1 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw5992step2 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5992 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw5993 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw5993step0 line 165
  34. def OAI.MUB6.Certificate.PairSemantics.raw5993step1 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw5993step2 line 169
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5993 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw5994 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw5994step0 line 190
  39. def OAI.MUB6.Certificate.PairSemantics.raw5994step1 line 192
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5994 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw5995 line 207
  42. def OAI.MUB6.Certificate.PairSemantics.raw5995step0 line 209
  43. def OAI.MUB6.Certificate.PairSemantics.raw5995step1 line 211
  44. def OAI.MUB6.Certificate.PairSemantics.raw5995step2 line 213
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5995 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw5996 line 232
  47. def OAI.MUB6.Certificate.PairSemantics.raw5996step0 line 234
  48. def OAI.MUB6.Certificate.PairSemantics.raw5996step1 line 236
  49. def OAI.MUB6.Certificate.PairSemantics.raw5996step2 line 238
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical5996 line 240
  51. def OAI.MUB6.Certificate.PairSemantics.raw5997 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw5997step0 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw5997step1 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw5997step2 line 263
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5997 line 265
  56. def OAI.MUB6.Certificate.PairSemantics.raw5998 line 282
  57. def OAI.MUB6.Certificate.PairSemantics.raw5998step0 line 284
  58. def OAI.MUB6.Certificate.PairSemantics.raw5998step1 line 286
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5998 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw5999 line 301
  61. def OAI.MUB6.Certificate.PairSemantics.raw5999step0 line 303
  62. def OAI.MUB6.Certificate.PairSemantics.raw5999step1 line 305
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5999 line 307
  64. def OAI.MUB6.Certificate.PairSemantics.raw6000 line 320
  65. def OAI.MUB6.Certificate.PairSemantics.raw6000step0 line 322
  66. def OAI.MUB6.Certificate.PairSemantics.raw6000step1 line 324
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6000 line 326
  68. def OAI.MUB6.Certificate.PairSemantics.raw6001 line 339
  69. def OAI.MUB6.Certificate.PairSemantics.raw6001step0 line 341
  70. def OAI.MUB6.Certificate.PairSemantics.raw6001step1 line 343
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6001 line 345
  72. def OAI.MUB6.Certificate.PairSemantics.raw6002 line 358
  73. def OAI.MUB6.Certificate.PairSemantics.raw6002step0 line 360
  74. def OAI.MUB6.Certificate.PairSemantics.raw6002step1 line 362
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6002 line 364
  76. def OAI.MUB6.Certificate.PairSemantics.raw6003 line 377
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6003 line 379
  78. def OAI.MUB6.Certificate.PairSemantics.raw6004 line 383
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6004 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw6005 line 389
  81. def OAI.MUB6.Certificate.PairSemantics.raw6005step0 line 391
  82. def OAI.MUB6.Certificate.PairSemantics.raw6005step1 line 393
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6005 line 395
  84. def OAI.MUB6.Certificate.PairSemantics.raw6006 line 408
  85. def OAI.MUB6.Certificate.PairSemantics.raw6006step0 line 410
  86. def OAI.MUB6.Certificate.PairSemantics.raw6006step1 line 412
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical6006 line 414
  88. def OAI.MUB6.Certificate.PairSemantics.raw6007 line 427
  89. def OAI.MUB6.Certificate.PairSemantics.raw6007step0 line 429
  90. def OAI.MUB6.Certificate.PairSemantics.raw6007step1 line 431
  91. def OAI.MUB6.Certificate.PairSemantics.raw6007step2 line 433
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical6007 line 435
  93. def OAI.MUB6.Certificate.PairSemantics.raw6008 line 452
  94. def OAI.MUB6.Certificate.PairSemantics.raw6008step0 line 454
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6008 line 456
  96. def OAI.MUB6.Certificate.PairSemantics.raw6009 line 465
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6009 line 467
  98. def OAI.MUB6.Certificate.PairSemantics.raw6010 line 471
  99. def OAI.MUB6.Certificate.PairSemantics.raw6010step0 line 473
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical6010 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw6011 line 484
  102. def OAI.MUB6.Certificate.PairSemantics.raw6011step0 line 486
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6011 line 488
  104. def OAI.MUB6.Certificate.PairSemantics.raw6012 line 497
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical6012 line 499
  106. def OAI.MUB6.Certificate.PairSemantics.raw6013 line 503
  107. def OAI.MUB6.Certificate.PairSemantics.raw6013step0 line 505
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6013 line 507
  109. def OAI.MUB6.Certificate.PairSemantics.raw6014 line 516
  110. def OAI.MUB6.Certificate.PairSemantics.raw6014step0 line 518
  111. def OAI.MUB6.Certificate.PairSemantics.raw6014step1 line 520
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical6014 line 522
  113. def OAI.MUB6.Certificate.PairSemantics.raw6015 line 535
  114. def OAI.MUB6.Certificate.PairSemantics.raw6015step0 line 537
  115. def OAI.MUB6.Certificate.PairSemantics.raw6015step1 line 539
  116. def OAI.MUB6.Certificate.PairSemantics.raw6015step2 line 541
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical6015 line 543