OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical93.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2976 line 20
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2976 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw2977 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw2977step0 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw2977step1 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2977 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw2978 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw2978step0 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw2978step1 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2978 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw2979 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw2979step0 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw2979step1 line 68
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical2979 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw2980 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw2980step0 line 85
  17. def OAI.MUB6.Certificate.PairSemantics.raw2980step1 line 87
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2980 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw2981 line 102
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical2981 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw2982 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw2982step0 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2982 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw2983 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw2983step0 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw2983step1 line 125
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2983 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw2984 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw2984step0 line 142
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2984 line 144
  31. def OAI.MUB6.Certificate.PairSemantics.raw2985 line 153
  32. def OAI.MUB6.Certificate.PairSemantics.raw2985step0 line 155
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2985 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw2986 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw2986step0 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw2986step1 line 170
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2986 line 172
  38. def OAI.MUB6.Certificate.PairSemantics.raw2987 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw2987step0 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw2987step1 line 189
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical2987 line 191
  42. def OAI.MUB6.Certificate.PairSemantics.raw2988 line 204
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2988 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw2989 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2989 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw2990 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw2990step0 line 218
  48. def OAI.MUB6.Certificate.PairSemantics.raw2990step1 line 220
  49. def OAI.MUB6.Certificate.PairSemantics.raw2990step2 line 222
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical2990 line 224
  51. def OAI.MUB6.Certificate.PairSemantics.raw2991 line 241
  52. def OAI.MUB6.Certificate.PairSemantics.raw2991step0 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw2991step1 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw2991step2 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2991 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw2992 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw2992step0 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw2992step1 line 270
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2992 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw2993 line 285
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2993 line 287
  62. def OAI.MUB6.Certificate.PairSemantics.raw2994 line 291
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2994 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw2995 line 297
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2995 line 299
  66. def OAI.MUB6.Certificate.PairSemantics.raw2996 line 303
  67. def OAI.MUB6.Certificate.PairSemantics.raw2996step0 line 305
  68. def OAI.MUB6.Certificate.PairSemantics.raw2996step1 line 307
  69. def OAI.MUB6.Certificate.PairSemantics.raw2996step2 line 309
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2996 line 311
  71. def OAI.MUB6.Certificate.PairSemantics.raw2997 line 328
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2997 line 330
  73. def OAI.MUB6.Certificate.PairSemantics.raw2998 line 334
  74. def OAI.MUB6.Certificate.PairSemantics.raw2998step0 line 336
  75. def OAI.MUB6.Certificate.PairSemantics.raw2998step1 line 338
  76. def OAI.MUB6.Certificate.PairSemantics.raw2998step2 line 340
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2998 line 342
  78. def OAI.MUB6.Certificate.PairSemantics.raw2999 line 359
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2999 line 361
  80. def OAI.MUB6.Certificate.PairSemantics.raw3000 line 365
  81. def OAI.MUB6.Certificate.PairSemantics.raw3000step0 line 367
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3000 line 369
  83. def OAI.MUB6.Certificate.PairSemantics.raw3001 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw3001step0 line 380
  85. def OAI.MUB6.Certificate.PairSemantics.raw3001step1 line 382
  86. def OAI.MUB6.Certificate.PairSemantics.raw3001step2 line 384
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3001 line 386
  88. def OAI.MUB6.Certificate.PairSemantics.raw3002 line 403
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3002 line 405
  90. def OAI.MUB6.Certificate.PairSemantics.raw3003 line 409
  91. def OAI.MUB6.Certificate.PairSemantics.raw3003step0 line 411
  92. def OAI.MUB6.Certificate.PairSemantics.raw3003step1 line 413
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3003 line 415
  94. def OAI.MUB6.Certificate.PairSemantics.raw3004 line 428
  95. def OAI.MUB6.Certificate.PairSemantics.raw3004step0 line 430
  96. def OAI.MUB6.Certificate.PairSemantics.raw3004step1 line 432
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3004 line 434
  98. def OAI.MUB6.Certificate.PairSemantics.raw3005 line 447
  99. def OAI.MUB6.Certificate.PairSemantics.raw3005step0 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw3005step1 line 451
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3005 line 453
  102. def OAI.MUB6.Certificate.PairSemantics.raw3006 line 466
  103. def OAI.MUB6.Certificate.PairSemantics.raw3006step0 line 468
  104. def OAI.MUB6.Certificate.PairSemantics.raw3006step1 line 470
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3006 line 472
  106. def OAI.MUB6.Certificate.PairSemantics.raw3007 line 485
  107. def OAI.MUB6.Certificate.PairSemantics.raw3007step0 line 487
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical3007 line 489