OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical104.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3328 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw3328step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical3328 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw3329 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw3329step0 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw3329step1 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3329 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw3330 line 50
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3330 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw3331 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3331 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw3332 line 62
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3332 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw3333 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw3333step0 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw3333step1 line 72
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3333 line 74
  18. def OAI.MUB6.Certificate.PairSemantics.raw3334 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw3334step0 line 89
  20. def OAI.MUB6.Certificate.PairSemantics.raw3334step1 line 91
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3334 line 93
  22. def OAI.MUB6.Certificate.PairSemantics.raw3335 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw3335step0 line 108
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3335 line 110
  25. def OAI.MUB6.Certificate.PairSemantics.raw3336 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw3336step0 line 121
  27. def OAI.MUB6.Certificate.PairSemantics.raw3336step1 line 123
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3336 line 125
  29. def OAI.MUB6.Certificate.PairSemantics.raw3337 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw3337step0 line 140
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3337 line 142
  32. def OAI.MUB6.Certificate.PairSemantics.raw3338 line 151
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3338 line 153
  34. def OAI.MUB6.Certificate.PairSemantics.raw3339 line 157
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3339 line 159
  36. def OAI.MUB6.Certificate.PairSemantics.raw3340 line 163
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3340 line 165
  38. def OAI.MUB6.Certificate.PairSemantics.raw3341 line 169
  39. def OAI.MUB6.Certificate.PairSemantics.raw3341step0 line 171
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical3341 line 173
  41. def OAI.MUB6.Certificate.PairSemantics.raw3342 line 182
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3342 line 184
  43. def OAI.MUB6.Certificate.PairSemantics.raw3343 line 188
  44. def OAI.MUB6.Certificate.PairSemantics.raw3343step0 line 190
  45. def OAI.MUB6.Certificate.PairSemantics.raw3343step1 line 192
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3343 line 194
  47. def OAI.MUB6.Certificate.PairSemantics.raw3344 line 207
  48. def OAI.MUB6.Certificate.PairSemantics.raw3344step0 line 209
  49. def OAI.MUB6.Certificate.PairSemantics.raw3344step1 line 211
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3344 line 213
  51. def OAI.MUB6.Certificate.PairSemantics.raw3345 line 226
  52. def OAI.MUB6.Certificate.PairSemantics.raw3345step0 line 228
  53. def OAI.MUB6.Certificate.PairSemantics.raw3345step1 line 230
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical3345 line 232
  55. def OAI.MUB6.Certificate.PairSemantics.raw3346 line 245
  56. def OAI.MUB6.Certificate.PairSemantics.raw3346step0 line 247
  57. def OAI.MUB6.Certificate.PairSemantics.raw3346step1 line 249
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical3346 line 251
  59. def OAI.MUB6.Certificate.PairSemantics.raw3347 line 264
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical3347 line 266
  61. def OAI.MUB6.Certificate.PairSemantics.raw3348 line 270
  62. def OAI.MUB6.Certificate.PairSemantics.raw3348step0 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw3348step1 line 274
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3348 line 276
  65. def OAI.MUB6.Certificate.PairSemantics.raw3349 line 289
  66. def OAI.MUB6.Certificate.PairSemantics.raw3349step0 line 291
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical3349 line 293
  68. def OAI.MUB6.Certificate.PairSemantics.raw3350 line 302
  69. def OAI.MUB6.Certificate.PairSemantics.raw3350step0 line 304
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3350 line 306
  71. def OAI.MUB6.Certificate.PairSemantics.raw3351 line 315
  72. def OAI.MUB6.Certificate.PairSemantics.raw3351step0 line 317
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3351 line 319
  74. def OAI.MUB6.Certificate.PairSemantics.raw3352 line 328
  75. def OAI.MUB6.Certificate.PairSemantics.raw3352step0 line 330
  76. def OAI.MUB6.Certificate.PairSemantics.raw3352step1 line 332
  77. def OAI.MUB6.Certificate.PairSemantics.raw3352step2 line 334
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical3352 line 336
  79. def OAI.MUB6.Certificate.PairSemantics.raw3353 line 354
  80. def OAI.MUB6.Certificate.PairSemantics.raw3353step0 line 356
  81. def OAI.MUB6.Certificate.PairSemantics.raw3353step1 line 358
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3353 line 360
  83. def OAI.MUB6.Certificate.PairSemantics.raw3354 line 373
  84. def OAI.MUB6.Certificate.PairSemantics.raw3354step0 line 375
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3354 line 377
  86. def OAI.MUB6.Certificate.PairSemantics.raw3355 line 386
  87. def OAI.MUB6.Certificate.PairSemantics.raw3355step0 line 388
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical3355 line 390
  89. def OAI.MUB6.Certificate.PairSemantics.raw3356 line 399
  90. def OAI.MUB6.Certificate.PairSemantics.raw3356step0 line 401
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical3356 line 403
  92. def OAI.MUB6.Certificate.PairSemantics.raw3357 line 412
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3357 line 414
  94. def OAI.MUB6.Certificate.PairSemantics.raw3358 line 418
  95. def OAI.MUB6.Certificate.PairSemantics.raw3358step0 line 420
  96. def OAI.MUB6.Certificate.PairSemantics.raw3358step1 line 422
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3358 line 424
  98. def OAI.MUB6.Certificate.PairSemantics.raw3359 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw3359step0 line 439
  100. def OAI.MUB6.Certificate.PairSemantics.raw3359step1 line 441
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3359 line 443