OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical123.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3936 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw3936step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw3936step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3936 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw3937 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw3937step0 line 42
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3937 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw3938 line 53
  9. def OAI.MUB6.Certificate.PairSemantics.raw3938step0 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw3938step1 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3938 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw3939 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw3939step0 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw3939step1 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3939 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw3940 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw3940step0 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw3940step1 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3940 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw3941 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw3941step0 line 112
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3941 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw3942 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw3942step0 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3942 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw3943 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3943 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw3944 line 142
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3944 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw3945 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw3945step0 line 150
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3945 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw3946 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw3946step0 line 163
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3946 line 165
  36. def OAI.MUB6.Certificate.PairSemantics.raw3947 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw3947step0 line 176
  38. def OAI.MUB6.Certificate.PairSemantics.raw3947step1 line 178
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3947 line 180
  40. def OAI.MUB6.Certificate.PairSemantics.raw3948 line 194
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3948 line 196
  42. def OAI.MUB6.Certificate.PairSemantics.raw3949 line 200
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3949 line 202
  44. def OAI.MUB6.Certificate.PairSemantics.raw3950 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw3950step0 line 208
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3950 line 210
  47. def OAI.MUB6.Certificate.PairSemantics.raw3951 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw3951step0 line 221
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3951 line 223
  50. def OAI.MUB6.Certificate.PairSemantics.raw3952 line 232
  51. def OAI.MUB6.Certificate.PairSemantics.raw3952step0 line 234
  52. def OAI.MUB6.Certificate.PairSemantics.raw3952step1 line 236
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3952 line 238
  54. def OAI.MUB6.Certificate.PairSemantics.raw3953 line 251
  55. def OAI.MUB6.Certificate.PairSemantics.raw3953step0 line 253
  56. def OAI.MUB6.Certificate.PairSemantics.raw3953step1 line 255
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3953 line 257
  58. def OAI.MUB6.Certificate.PairSemantics.raw3954 line 270
  59. def OAI.MUB6.Certificate.PairSemantics.raw3954step0 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw3954step1 line 274
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3954 line 276
  62. def OAI.MUB6.Certificate.PairSemantics.raw3955 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw3955step0 line 291
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3955 line 293
  65. def OAI.MUB6.Certificate.PairSemantics.raw3956 line 302
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3956 line 304
  67. def OAI.MUB6.Certificate.PairSemantics.raw3957 line 308
  68. def OAI.MUB6.Certificate.PairSemantics.raw3957step0 line 310
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3957 line 312
  70. def OAI.MUB6.Certificate.PairSemantics.raw3958 line 321
  71. def OAI.MUB6.Certificate.PairSemantics.raw3958step0 line 323
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3958 line 325
  73. def OAI.MUB6.Certificate.PairSemantics.raw3959 line 334
  74. def OAI.MUB6.Certificate.PairSemantics.raw3959step0 line 336
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3959 line 338
  76. def OAI.MUB6.Certificate.PairSemantics.raw3960 line 347
  77. def OAI.MUB6.Certificate.PairSemantics.raw3960step0 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw3960step1 line 351
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3960 line 353
  80. def OAI.MUB6.Certificate.PairSemantics.raw3961 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw3961step0 line 368
  82. def OAI.MUB6.Certificate.PairSemantics.raw3961step1 line 370
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3961 line 372
  84. def OAI.MUB6.Certificate.PairSemantics.raw3962 line 385
  85. def OAI.MUB6.Certificate.PairSemantics.raw3962step0 line 387
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3962 line 389
  87. def OAI.MUB6.Certificate.PairSemantics.raw3963 line 398
  88. def OAI.MUB6.Certificate.PairSemantics.raw3963step0 line 400
  89. def OAI.MUB6.Certificate.PairSemantics.raw3963step1 line 402
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3963 line 404
  91. def OAI.MUB6.Certificate.PairSemantics.raw3964 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw3964step0 line 419
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3964 line 421
  94. def OAI.MUB6.Certificate.PairSemantics.raw3965 line 430
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical3965 line 432
  96. def OAI.MUB6.Certificate.PairSemantics.raw3966 line 436
  97. def OAI.MUB6.Certificate.PairSemantics.raw3966step0 line 438
  98. def OAI.MUB6.Certificate.PairSemantics.raw3966step1 line 440
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical3966 line 442
  100. def OAI.MUB6.Certificate.PairSemantics.raw3967 line 455
  101. def OAI.MUB6.Certificate.PairSemantics.raw3967step0 line 457
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3967 line 459