OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical140.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4480 line 19
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4480 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw4481 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw4481step0 line 27
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4481 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw4482 line 38
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4482 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw4483 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4483 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw4484 line 50
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4484 line 52
  12. def OAI.MUB6.Certificate.PairSemantics.raw4485 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw4485step0 line 58
  14. def OAI.MUB6.Certificate.PairSemantics.raw4485step1 line 60
  15. def OAI.MUB6.Certificate.PairSemantics.raw4485step2 line 62
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4485 line 64
  17. def OAI.MUB6.Certificate.PairSemantics.raw4486 line 81
  18. def OAI.MUB6.Certificate.PairSemantics.raw4486step0 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw4486step1 line 85
  20. def OAI.MUB6.Certificate.PairSemantics.raw4486step2 line 87
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4486 line 89
  22. def OAI.MUB6.Certificate.PairSemantics.raw4487 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw4487step0 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw4487step1 line 110
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4487 line 112
  26. def OAI.MUB6.Certificate.PairSemantics.raw4488 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw4488step0 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw4488step1 line 129
  29. def OAI.MUB6.Certificate.PairSemantics.raw4488step2 line 131
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4488 line 133
  31. def OAI.MUB6.Certificate.PairSemantics.raw4489 line 150
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4489 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw4490 line 156
  34. def OAI.MUB6.Certificate.PairSemantics.raw4490step0 line 158
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4490 line 160
  36. def OAI.MUB6.Certificate.PairSemantics.raw4491 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw4491step0 line 171
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4491 line 173
  39. def OAI.MUB6.Certificate.PairSemantics.raw4492 line 182
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4492 line 184
  41. def OAI.MUB6.Certificate.PairSemantics.raw4493 line 188
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4493 line 190
  43. def OAI.MUB6.Certificate.PairSemantics.raw4494 line 194
  44. def OAI.MUB6.Certificate.PairSemantics.raw4494step0 line 196
  45. def OAI.MUB6.Certificate.PairSemantics.raw4494step1 line 198
  46. def OAI.MUB6.Certificate.PairSemantics.raw4494step2 line 200
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4494 line 202
  48. def OAI.MUB6.Certificate.PairSemantics.raw4495 line 219
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical4495 line 221
  50. def OAI.MUB6.Certificate.PairSemantics.raw4496 line 225
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4496 line 227
  52. def OAI.MUB6.Certificate.PairSemantics.raw4497 line 231
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4497 line 233
  54. def OAI.MUB6.Certificate.PairSemantics.raw4498 line 237
  55. def OAI.MUB6.Certificate.PairSemantics.raw4498step0 line 239
  56. def OAI.MUB6.Certificate.PairSemantics.raw4498step1 line 241
  57. def OAI.MUB6.Certificate.PairSemantics.raw4498step2 line 243
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4498 line 245
  59. def OAI.MUB6.Certificate.PairSemantics.raw4499 line 262
  60. def OAI.MUB6.Certificate.PairSemantics.raw4499step0 line 264
  61. def OAI.MUB6.Certificate.PairSemantics.raw4499step1 line 266
  62. def OAI.MUB6.Certificate.PairSemantics.raw4499step2 line 268
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical4499 line 270
  64. def OAI.MUB6.Certificate.PairSemantics.raw4500 line 287
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4500 line 289
  66. def OAI.MUB6.Certificate.PairSemantics.raw4501 line 293
  67. def OAI.MUB6.Certificate.PairSemantics.raw4501step0 line 295
  68. def OAI.MUB6.Certificate.PairSemantics.raw4501step1 line 297
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4501 line 299
  70. def OAI.MUB6.Certificate.PairSemantics.raw4502 line 312
  71. def OAI.MUB6.Certificate.PairSemantics.raw4502step0 line 314
  72. def OAI.MUB6.Certificate.PairSemantics.raw4502step1 line 316
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4502 line 318
  74. def OAI.MUB6.Certificate.PairSemantics.raw4503 line 331
  75. def OAI.MUB6.Certificate.PairSemantics.raw4503step0 line 333
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4503 line 335
  77. def OAI.MUB6.Certificate.PairSemantics.raw4504 line 344
  78. def OAI.MUB6.Certificate.PairSemantics.raw4504step0 line 346
  79. def OAI.MUB6.Certificate.PairSemantics.raw4504step1 line 348
  80. def OAI.MUB6.Certificate.PairSemantics.raw4504step2 line 350
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4504 line 352
  82. def OAI.MUB6.Certificate.PairSemantics.raw4505 line 369
  83. def OAI.MUB6.Certificate.PairSemantics.raw4505step0 line 371
  84. def OAI.MUB6.Certificate.PairSemantics.raw4505step1 line 373
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4505 line 375
  86. def OAI.MUB6.Certificate.PairSemantics.raw4506 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw4506step0 line 390
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4506 line 392
  89. def OAI.MUB6.Certificate.PairSemantics.raw4507 line 401
  90. def OAI.MUB6.Certificate.PairSemantics.raw4507step0 line 403
  91. def OAI.MUB6.Certificate.PairSemantics.raw4507step1 line 405
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical4507 line 407
  93. def OAI.MUB6.Certificate.PairSemantics.raw4508 line 420
  94. def OAI.MUB6.Certificate.PairSemantics.raw4508step0 line 422
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical4508 line 424
  96. def OAI.MUB6.Certificate.PairSemantics.raw4509 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw4509step0 line 435
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical4509 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw4510 line 446
  100. def OAI.MUB6.Certificate.PairSemantics.raw4510step0 line 448
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4510 line 450
  102. def OAI.MUB6.Certificate.PairSemantics.raw4511 line 459
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4511 line 461