OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical132.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4224 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw4224step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw4224step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4224 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw4225 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw4225step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw4225step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4225 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw4226 line 59
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4226 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw4227 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw4227step0 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw4227step1 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4227 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw4228 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw4228step0 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw4228step1 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4228 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw4229 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw4229step0 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw4229step1 line 107
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4229 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw4230 line 122
  24. def OAI.MUB6.Certificate.PairSemantics.raw4230step0 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw4230step1 line 126
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4230 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw4231 line 141
  28. def OAI.MUB6.Certificate.PairSemantics.raw4231step0 line 143
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4231 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw4232 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw4232step0 line 156
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4232 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw4233 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw4233step0 line 169
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4233 line 171
  36. def OAI.MUB6.Certificate.PairSemantics.raw4234 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw4234step0 line 182
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4234 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw4235 line 193
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4235 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw4236 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw4236step0 line 201
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4236 line 203
  44. def OAI.MUB6.Certificate.PairSemantics.raw4237 line 212
  45. def OAI.MUB6.Certificate.PairSemantics.raw4237step0 line 214
  46. def OAI.MUB6.Certificate.PairSemantics.raw4237step1 line 216
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4237 line 218
  48. def OAI.MUB6.Certificate.PairSemantics.raw4238 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw4238step0 line 233
  50. def OAI.MUB6.Certificate.PairSemantics.raw4238step1 line 235
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4238 line 237
  52. def OAI.MUB6.Certificate.PairSemantics.raw4239 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw4239step0 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw4239step1 line 254
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4239 line 256
  56. def OAI.MUB6.Certificate.PairSemantics.raw4240 line 269
  57. def OAI.MUB6.Certificate.PairSemantics.raw4240step0 line 271
  58. def OAI.MUB6.Certificate.PairSemantics.raw4240step1 line 273
  59. def OAI.MUB6.Certificate.PairSemantics.raw4240step2 line 275
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical4240 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw4241 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw4241step0 line 296
  63. def OAI.MUB6.Certificate.PairSemantics.raw4241step1 line 298
  64. def OAI.MUB6.Certificate.PairSemantics.raw4241step2 line 300
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4241 line 302
  66. def OAI.MUB6.Certificate.PairSemantics.raw4242 line 319
  67. def OAI.MUB6.Certificate.PairSemantics.raw4242step0 line 321
  68. def OAI.MUB6.Certificate.PairSemantics.raw4242step1 line 323
  69. def OAI.MUB6.Certificate.PairSemantics.raw4242step2 line 325
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4242 line 327
  71. def OAI.MUB6.Certificate.PairSemantics.raw4243 line 344
  72. def OAI.MUB6.Certificate.PairSemantics.raw4243step0 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw4243step1 line 348
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4243 line 350
  75. def OAI.MUB6.Certificate.PairSemantics.raw4244 line 363
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4244 line 365
  77. def OAI.MUB6.Certificate.PairSemantics.raw4245 line 369
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical4245 line 371
  79. def OAI.MUB6.Certificate.PairSemantics.raw4246 line 375
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4246 line 377
  81. def OAI.MUB6.Certificate.PairSemantics.raw4247 line 381
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4247 line 383
  83. def OAI.MUB6.Certificate.PairSemantics.raw4248 line 387
  84. def OAI.MUB6.Certificate.PairSemantics.raw4248step0 line 389
  85. def OAI.MUB6.Certificate.PairSemantics.raw4248step1 line 391
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4248 line 393
  87. def OAI.MUB6.Certificate.PairSemantics.raw4249 line 406
  88. def OAI.MUB6.Certificate.PairSemantics.raw4249step0 line 408
  89. def OAI.MUB6.Certificate.PairSemantics.raw4249step1 line 410
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4249 line 412
  91. def OAI.MUB6.Certificate.PairSemantics.raw4250 line 425
  92. def OAI.MUB6.Certificate.PairSemantics.raw4250step0 line 427
  93. def OAI.MUB6.Certificate.PairSemantics.raw4250step1 line 429
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4250 line 431
  95. def OAI.MUB6.Certificate.PairSemantics.raw4251 line 444
  96. def OAI.MUB6.Certificate.PairSemantics.raw4251step0 line 446
  97. def OAI.MUB6.Certificate.PairSemantics.raw4251step1 line 448
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical4251 line 450
  99. def OAI.MUB6.Certificate.PairSemantics.raw4252 line 463
  100. def OAI.MUB6.Certificate.PairSemantics.raw4252step0 line 465
  101. def OAI.MUB6.Certificate.PairSemantics.raw4252step1 line 467
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4252 line 469
  103. def OAI.MUB6.Certificate.PairSemantics.raw4253 line 482
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4253 line 484
  105. def OAI.MUB6.Certificate.PairSemantics.raw4254 line 488
  106. def OAI.MUB6.Certificate.PairSemantics.raw4254step0 line 490
  107. def OAI.MUB6.Certificate.PairSemantics.raw4254step1 line 492
  108. def OAI.MUB6.Certificate.PairSemantics.raw4254step2 line 494
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical4254 line 496
  110. def OAI.MUB6.Certificate.PairSemantics.raw4255 line 513
  111. def OAI.MUB6.Certificate.PairSemantics.raw4255step0 line 515
  112. def OAI.MUB6.Certificate.PairSemantics.raw4255step1 line 517
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical4255 line 519