OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical310.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9920 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw9920step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9920 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw9921 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw9921step0 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw9921step1 line 33
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical9921 line 35
  8. def OAI.MUB6.Certificate.PairSemantics.raw9922 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw9922step0 line 50
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9922 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw9923 line 61
  12. def OAI.MUB6.Certificate.PairSemantics.raw9923step0 line 63
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical9923 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw9924 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw9924step0 line 76
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical9924 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw9925 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw9925step0 line 89
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9925 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw9926 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw9926step0 line 102
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9926 line 104
  23. def OAI.MUB6.Certificate.PairSemantics.raw9927 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw9927step0 line 115
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical9927 line 117
  26. def OAI.MUB6.Certificate.PairSemantics.raw9928 line 126
  27. def OAI.MUB6.Certificate.PairSemantics.raw9928step0 line 128
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9928 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw9929 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw9929step0 line 141
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9929 line 143
  32. def OAI.MUB6.Certificate.PairSemantics.raw9930 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw9930step0 line 154
  34. def OAI.MUB6.Certificate.PairSemantics.raw9930step1 line 156
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9930 line 158
  36. def OAI.MUB6.Certificate.PairSemantics.raw9931 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw9931step0 line 173
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9931 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw9932 line 184
  40. def OAI.MUB6.Certificate.PairSemantics.raw9932step0 line 186
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9932 line 188
  42. def OAI.MUB6.Certificate.PairSemantics.raw9933 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw9933step0 line 199
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9933 line 201
  45. def OAI.MUB6.Certificate.PairSemantics.raw9934 line 210
  46. def OAI.MUB6.Certificate.PairSemantics.raw9934step0 line 212
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9934 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw9935 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw9935step0 line 225
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9935 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw9936 line 236
  52. def OAI.MUB6.Certificate.PairSemantics.raw9936step0 line 238
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9936 line 240
  54. def OAI.MUB6.Certificate.PairSemantics.raw9937 line 249
  55. def OAI.MUB6.Certificate.PairSemantics.raw9937step0 line 251
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9937 line 253
  57. def OAI.MUB6.Certificate.PairSemantics.raw9938 line 262
  58. def OAI.MUB6.Certificate.PairSemantics.raw9938step0 line 264
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9938 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw9939 line 275
  61. def OAI.MUB6.Certificate.PairSemantics.raw9939step0 line 277
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9939 line 279
  63. def OAI.MUB6.Certificate.PairSemantics.raw9940 line 288
  64. def OAI.MUB6.Certificate.PairSemantics.raw9940step0 line 290
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9940 line 292
  66. def OAI.MUB6.Certificate.PairSemantics.raw9941 line 301
  67. def OAI.MUB6.Certificate.PairSemantics.raw9941step0 line 303
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9941 line 305
  69. def OAI.MUB6.Certificate.PairSemantics.raw9942 line 314
  70. def OAI.MUB6.Certificate.PairSemantics.raw9942step0 line 316
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9942 line 318
  72. def OAI.MUB6.Certificate.PairSemantics.raw9943 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw9943step0 line 329
  74. def OAI.MUB6.Certificate.PairSemantics.raw9943step1 line 331
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9943 line 333
  76. def OAI.MUB6.Certificate.PairSemantics.raw9944 line 346
  77. def OAI.MUB6.Certificate.PairSemantics.raw9944step0 line 348
  78. def OAI.MUB6.Certificate.PairSemantics.raw9944step1 line 350
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical9944 line 352
  80. def OAI.MUB6.Certificate.PairSemantics.raw9945 line 365
  81. def OAI.MUB6.Certificate.PairSemantics.raw9945step0 line 367
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9945 line 369
  83. def OAI.MUB6.Certificate.PairSemantics.raw9946 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw9946step0 line 380
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9946 line 382
  86. def OAI.MUB6.Certificate.PairSemantics.raw9947 line 391
  87. def OAI.MUB6.Certificate.PairSemantics.raw9947step0 line 393
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9947 line 395
  89. def OAI.MUB6.Certificate.PairSemantics.raw9948 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw9948step0 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw9948step1 line 408
  92. def OAI.MUB6.Certificate.PairSemantics.raw9948step2 line 410
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9948 line 412
  94. def OAI.MUB6.Certificate.PairSemantics.raw9949 line 429
  95. def OAI.MUB6.Certificate.PairSemantics.raw9949step0 line 431
  96. def OAI.MUB6.Certificate.PairSemantics.raw9949step1 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw9949step2 line 435
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9949 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw9950 line 454
  100. def OAI.MUB6.Certificate.PairSemantics.raw9950step0 line 456
  101. def OAI.MUB6.Certificate.PairSemantics.raw9950step1 line 458
  102. def OAI.MUB6.Certificate.PairSemantics.raw9950step2 line 460
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical9950 line 462
  104. def OAI.MUB6.Certificate.PairSemantics.raw9951 line 479
  105. def OAI.MUB6.Certificate.PairSemantics.raw9951step0 line 481
  106. def OAI.MUB6.Certificate.PairSemantics.raw9951step1 line 483
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9951 line 485