OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical92.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2944 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2944 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw2945 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw2945step0 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2945 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw2946 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw2946step0 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw2946step1 line 41
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2946 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw2947 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2947 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw2948 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw2948step0 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw2948step1 line 66
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2948 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw2949 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw2949step0 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw2949step1 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2949 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw2950 line 100
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2950 line 102
  22. def OAI.MUB6.Certificate.PairSemantics.raw2951 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical2951 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw2952 line 112
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2952 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw2953 line 118
  27. def OAI.MUB6.Certificate.PairSemantics.raw2953step0 line 120
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2953 line 122
  29. def OAI.MUB6.Certificate.PairSemantics.raw2954 line 131
  30. def OAI.MUB6.Certificate.PairSemantics.raw2954step0 line 133
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2954 line 135
  32. def OAI.MUB6.Certificate.PairSemantics.raw2955 line 144
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2955 line 146
  34. def OAI.MUB6.Certificate.PairSemantics.raw2956 line 150
  35. def OAI.MUB6.Certificate.PairSemantics.raw2956step0 line 152
  36. def OAI.MUB6.Certificate.PairSemantics.raw2956step1 line 154
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2956 line 156
  38. def OAI.MUB6.Certificate.PairSemantics.raw2957 line 169
  39. def OAI.MUB6.Certificate.PairSemantics.raw2957step0 line 171
  40. def OAI.MUB6.Certificate.PairSemantics.raw2957step1 line 173
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical2957 line 175
  42. def OAI.MUB6.Certificate.PairSemantics.raw2958 line 188
  43. def OAI.MUB6.Certificate.PairSemantics.raw2958step0 line 190
  44. def OAI.MUB6.Certificate.PairSemantics.raw2958step1 line 192
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2958 line 194
  46. def OAI.MUB6.Certificate.PairSemantics.raw2959 line 207
  47. def OAI.MUB6.Certificate.PairSemantics.raw2959step0 line 209
  48. def OAI.MUB6.Certificate.PairSemantics.raw2959step1 line 211
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2959 line 213
  50. def OAI.MUB6.Certificate.PairSemantics.raw2960 line 226
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2960 line 228
  52. def OAI.MUB6.Certificate.PairSemantics.raw2961 line 232
  53. def OAI.MUB6.Certificate.PairSemantics.raw2961step0 line 234
  54. def OAI.MUB6.Certificate.PairSemantics.raw2961step1 line 236
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2961 line 238
  56. def OAI.MUB6.Certificate.PairSemantics.raw2962 line 251
  57. def OAI.MUB6.Certificate.PairSemantics.raw2962step0 line 253
  58. def OAI.MUB6.Certificate.PairSemantics.raw2962step1 line 255
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2962 line 257
  60. def OAI.MUB6.Certificate.PairSemantics.raw2963 line 270
  61. def OAI.MUB6.Certificate.PairSemantics.raw2963step0 line 272
  62. def OAI.MUB6.Certificate.PairSemantics.raw2963step1 line 274
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2963 line 276
  64. def OAI.MUB6.Certificate.PairSemantics.raw2964 line 289
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2964 line 291
  66. def OAI.MUB6.Certificate.PairSemantics.raw2965 line 295
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2965 line 297
  68. def OAI.MUB6.Certificate.PairSemantics.raw2966 line 301
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2966 line 303
  70. def OAI.MUB6.Certificate.PairSemantics.raw2967 line 307
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2967 line 309
  72. def OAI.MUB6.Certificate.PairSemantics.raw2968 line 313
  73. def OAI.MUB6.Certificate.PairSemantics.raw2968step0 line 315
  74. def OAI.MUB6.Certificate.PairSemantics.raw2968step1 line 317
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2968 line 319
  76. def OAI.MUB6.Certificate.PairSemantics.raw2969 line 332
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2969 line 334
  78. def OAI.MUB6.Certificate.PairSemantics.raw2970 line 338
  79. def OAI.MUB6.Certificate.PairSemantics.raw2970step0 line 340
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2970 line 342
  81. def OAI.MUB6.Certificate.PairSemantics.raw2971 line 351
  82. def OAI.MUB6.Certificate.PairSemantics.raw2971step0 line 353
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2971 line 355
  84. def OAI.MUB6.Certificate.PairSemantics.raw2972 line 364
  85. def OAI.MUB6.Certificate.PairSemantics.raw2972step0 line 366
  86. def OAI.MUB6.Certificate.PairSemantics.raw2972step1 line 368
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2972 line 370
  88. def OAI.MUB6.Certificate.PairSemantics.raw2973 line 383
  89. def OAI.MUB6.Certificate.PairSemantics.raw2973step0 line 385
  90. def OAI.MUB6.Certificate.PairSemantics.raw2973step1 line 387
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical2973 line 389
  92. def OAI.MUB6.Certificate.PairSemantics.raw2974 line 402
  93. def OAI.MUB6.Certificate.PairSemantics.raw2974step0 line 404
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2974 line 406
  95. def OAI.MUB6.Certificate.PairSemantics.raw2975 line 415
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical2975 line 417