OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical31.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw992 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw992step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw992step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical992 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw993 line 35
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical993 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw994 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw994step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical994 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw995 line 54
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical995 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw996 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical996 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw997 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw997step0 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw997step1 line 70
  17. def OAI.MUB6.Certificate.PairSemantics.raw997step2 line 72
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical997 line 74
  19. def OAI.MUB6.Certificate.PairSemantics.raw998 line 91
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical998 line 93
  21. def OAI.MUB6.Certificate.PairSemantics.raw999 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw999step0 line 99
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical999 line 101
  24. def OAI.MUB6.Certificate.PairSemantics.raw1000 line 110
  25. def OAI.MUB6.Certificate.PairSemantics.raw1000step0 line 112
  26. def OAI.MUB6.Certificate.PairSemantics.raw1000step1 line 114
  27. def OAI.MUB6.Certificate.PairSemantics.raw1000step2 line 116
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1000 line 118
  29. def OAI.MUB6.Certificate.PairSemantics.raw1001 line 135
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1001 line 137
  31. def OAI.MUB6.Certificate.PairSemantics.raw1002 line 141
  32. def OAI.MUB6.Certificate.PairSemantics.raw1002step0 line 143
  33. def OAI.MUB6.Certificate.PairSemantics.raw1002step1 line 145
  34. def OAI.MUB6.Certificate.PairSemantics.raw1002step2 line 147
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1002 line 149
  36. def OAI.MUB6.Certificate.PairSemantics.raw1003 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw1003step0 line 168
  38. def OAI.MUB6.Certificate.PairSemantics.raw1003step1 line 170
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1003 line 172
  40. def OAI.MUB6.Certificate.PairSemantics.raw1004 line 185
  41. def OAI.MUB6.Certificate.PairSemantics.raw1004step0 line 187
  42. def OAI.MUB6.Certificate.PairSemantics.raw1004step1 line 189
  43. def OAI.MUB6.Certificate.PairSemantics.raw1004step2 line 191
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1004 line 193
  45. def OAI.MUB6.Certificate.PairSemantics.raw1005 line 210
  46. def OAI.MUB6.Certificate.PairSemantics.raw1005step0 line 212
  47. def OAI.MUB6.Certificate.PairSemantics.raw1005step1 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw1005step2 line 216
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1005 line 218
  50. def OAI.MUB6.Certificate.PairSemantics.raw1006 line 235
  51. def OAI.MUB6.Certificate.PairSemantics.raw1006step0 line 237
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1006 line 239
  53. def OAI.MUB6.Certificate.PairSemantics.raw1007 line 248
  54. def OAI.MUB6.Certificate.PairSemantics.raw1007step0 line 250
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1007 line 252
  56. def OAI.MUB6.Certificate.PairSemantics.raw1008 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw1008step0 line 263
  58. def OAI.MUB6.Certificate.PairSemantics.raw1008step1 line 265
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1008 line 267
  60. def OAI.MUB6.Certificate.PairSemantics.raw1009 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw1009step0 line 282
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1009 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw1010 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw1010step0 line 295
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1010 line 297
  66. def OAI.MUB6.Certificate.PairSemantics.raw1011 line 306
  67. def OAI.MUB6.Certificate.PairSemantics.raw1011step0 line 308
  68. def OAI.MUB6.Certificate.PairSemantics.raw1011step1 line 310
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1011 line 312
  70. def OAI.MUB6.Certificate.PairSemantics.raw1012 line 325
  71. def OAI.MUB6.Certificate.PairSemantics.raw1012step0 line 327
  72. def OAI.MUB6.Certificate.PairSemantics.raw1012step1 line 329
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1012 line 331
  74. def OAI.MUB6.Certificate.PairSemantics.raw1013 line 344
  75. def OAI.MUB6.Certificate.PairSemantics.raw1013step0 line 346
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1013 line 348
  77. def OAI.MUB6.Certificate.PairSemantics.raw1014 line 357
  78. def OAI.MUB6.Certificate.PairSemantics.raw1014step0 line 359
  79. def OAI.MUB6.Certificate.PairSemantics.raw1014step1 line 361
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1014 line 363
  81. def OAI.MUB6.Certificate.PairSemantics.raw1015 line 376
  82. def OAI.MUB6.Certificate.PairSemantics.raw1015step0 line 378
  83. def OAI.MUB6.Certificate.PairSemantics.raw1015step1 line 380
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical1015 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw1016 line 395
  86. def OAI.MUB6.Certificate.PairSemantics.raw1016step0 line 397
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1016 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw1017 line 408
  89. def OAI.MUB6.Certificate.PairSemantics.raw1017step0 line 410
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1017 line 412
  91. def OAI.MUB6.Certificate.PairSemantics.raw1018 line 421
  92. def OAI.MUB6.Certificate.PairSemantics.raw1018step0 line 423
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1018 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw1019 line 434
  95. def OAI.MUB6.Certificate.PairSemantics.raw1019step0 line 436
  96. def OAI.MUB6.Certificate.PairSemantics.raw1019step1 line 438
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1019 line 440
  98. def OAI.MUB6.Certificate.PairSemantics.raw1020 line 453
  99. def OAI.MUB6.Certificate.PairSemantics.raw1020step0 line 455
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical1020 line 457
  101. def OAI.MUB6.Certificate.PairSemantics.raw1021 line 466
  102. def OAI.MUB6.Certificate.PairSemantics.raw1021step0 line 468
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical1021 line 470
  104. def OAI.MUB6.Certificate.PairSemantics.raw1022 line 479
  105. def OAI.MUB6.Certificate.PairSemantics.raw1022step0 line 481
  106. def OAI.MUB6.Certificate.PairSemantics.raw1022step1 line 483
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical1022 line 485
  108. def OAI.MUB6.Certificate.PairSemantics.raw1023 line 498
  109. def OAI.MUB6.Certificate.PairSemantics.raw1023step0 line 500
  110. def OAI.MUB6.Certificate.PairSemantics.raw1023step1 line 502
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical1023 line 504