OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical96.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3072 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw3072step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw3072step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3072 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw3073 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw3073step0 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw3073step1 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3073 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw3074 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw3074step0 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw3074step1 line 60
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3074 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw3075 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw3075step0 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw3075step1 line 79
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3075 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw3076 line 94
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3076 line 96
  19. def OAI.MUB6.Certificate.PairSemantics.raw3077 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3077 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw3078 line 106
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3078 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw3079 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw3079step0 line 114
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3079 line 116
  26. def OAI.MUB6.Certificate.PairSemantics.raw3080 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw3080step0 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw3080step1 line 129
  29. def OAI.MUB6.Certificate.PairSemantics.raw3080step2 line 131
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3080 line 133
  31. def OAI.MUB6.Certificate.PairSemantics.raw3081 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw3081step0 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw3081step1 line 154
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3081 line 156
  35. def OAI.MUB6.Certificate.PairSemantics.raw3082 line 169
  36. def OAI.MUB6.Certificate.PairSemantics.raw3082step0 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw3082step1 line 173
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3082 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw3083 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw3083step0 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw3083step1 line 192
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3083 line 194
  43. def OAI.MUB6.Certificate.PairSemantics.raw3084 line 207
  44. def OAI.MUB6.Certificate.PairSemantics.raw3084step0 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw3084step1 line 211
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3084 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw3085 line 226
  48. def OAI.MUB6.Certificate.PairSemantics.raw3085step0 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw3085step1 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw3085step2 line 232
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3085 line 234
  52. def OAI.MUB6.Certificate.PairSemantics.raw3086 line 251
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3086 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw3087 line 257
  55. def OAI.MUB6.Certificate.PairSemantics.raw3087step0 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw3087step1 line 261
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3087 line 263
  58. def OAI.MUB6.Certificate.PairSemantics.raw3088 line 276
  59. def OAI.MUB6.Certificate.PairSemantics.raw3088step0 line 278
  60. def OAI.MUB6.Certificate.PairSemantics.raw3088step1 line 280
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3088 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw3089 line 295
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical3089 line 297
  64. def OAI.MUB6.Certificate.PairSemantics.raw3090 line 301
  65. def OAI.MUB6.Certificate.PairSemantics.raw3090step0 line 303
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3090 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw3091 line 314
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3091 line 316
  69. def OAI.MUB6.Certificate.PairSemantics.raw3092 line 320
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3092 line 322
  71. def OAI.MUB6.Certificate.PairSemantics.raw3093 line 326
  72. def OAI.MUB6.Certificate.PairSemantics.raw3093step0 line 328
  73. def OAI.MUB6.Certificate.PairSemantics.raw3093step1 line 330
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical3093 line 332
  75. def OAI.MUB6.Certificate.PairSemantics.raw3094 line 345
  76. def OAI.MUB6.Certificate.PairSemantics.raw3094step0 line 347
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3094 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw3095 line 358
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3095 line 360
  80. def OAI.MUB6.Certificate.PairSemantics.raw3096 line 364
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical3096 line 366
  82. def OAI.MUB6.Certificate.PairSemantics.raw3097 line 370
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3097 line 372
  84. def OAI.MUB6.Certificate.PairSemantics.raw3098 line 376
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3098 line 378
  86. def OAI.MUB6.Certificate.PairSemantics.raw3099 line 382
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3099 line 384
  88. def OAI.MUB6.Certificate.PairSemantics.raw3100 line 388
  89. def OAI.MUB6.Certificate.PairSemantics.raw3100step0 line 390
  90. def OAI.MUB6.Certificate.PairSemantics.raw3100step1 line 392
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3100 line 394
  92. def OAI.MUB6.Certificate.PairSemantics.raw3101 line 407
  93. def OAI.MUB6.Certificate.PairSemantics.raw3101step0 line 409
  94. def OAI.MUB6.Certificate.PairSemantics.raw3101step1 line 411
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical3101 line 413
  96. def OAI.MUB6.Certificate.PairSemantics.raw3102 line 426
  97. def OAI.MUB6.Certificate.PairSemantics.raw3102step0 line 428
  98. def OAI.MUB6.Certificate.PairSemantics.raw3102step1 line 430
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3102 line 432
  100. def OAI.MUB6.Certificate.PairSemantics.raw3103 line 445
  101. def OAI.MUB6.Certificate.PairSemantics.raw3103step0 line 447
  102. def OAI.MUB6.Certificate.PairSemantics.raw3103step1 line 449
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3103 line 451