OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical202.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6464 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw6464step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6464 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw6465 line 31
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6465 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw6466 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw6466step0 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6466 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw6467 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw6467step0 line 52
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6467 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw6468 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw6468step0 line 65
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6468 line 67
  15. def OAI.MUB6.Certificate.PairSemantics.raw6469 line 76
  16. def OAI.MUB6.Certificate.PairSemantics.raw6469step0 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw6469step1 line 80
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6469 line 82
  19. def OAI.MUB6.Certificate.PairSemantics.raw6470 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw6470step0 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw6470step1 line 99
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6470 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw6471 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw6471step0 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw6471step1 line 118
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6471 line 120
  27. def OAI.MUB6.Certificate.PairSemantics.raw6472 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw6472step0 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw6472step1 line 137
  30. def OAI.MUB6.Certificate.PairSemantics.raw6472step2 line 139
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6472 line 141
  32. def OAI.MUB6.Certificate.PairSemantics.raw6473 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw6473step0 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw6473step1 line 162
  35. def OAI.MUB6.Certificate.PairSemantics.raw6473step2 line 164
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6473 line 166
  37. def OAI.MUB6.Certificate.PairSemantics.raw6474 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw6474step0 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw6474step1 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw6474step2 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw6474step3 line 192
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6474 line 194
  43. def OAI.MUB6.Certificate.PairSemantics.raw6475 line 216
  44. def OAI.MUB6.Certificate.PairSemantics.raw6475step0 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw6475step1 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw6475step2 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw6475step3 line 224
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6475 line 226
  49. def OAI.MUB6.Certificate.PairSemantics.raw6476 line 249
  50. def OAI.MUB6.Certificate.PairSemantics.raw6476step0 line 251
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6476 line 253
  52. def OAI.MUB6.Certificate.PairSemantics.raw6477 line 263
  53. def OAI.MUB6.Certificate.PairSemantics.raw6477step0 line 265
  54. def OAI.MUB6.Certificate.PairSemantics.raw6477step1 line 267
  55. def OAI.MUB6.Certificate.PairSemantics.raw6477step2 line 269
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6477 line 271
  57. def OAI.MUB6.Certificate.PairSemantics.raw6478 line 289
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6478 line 291
  59. def OAI.MUB6.Certificate.PairSemantics.raw6479 line 295
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6479 line 297
  61. def OAI.MUB6.Certificate.PairSemantics.raw6480 line 301
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6480 line 303
  63. def OAI.MUB6.Certificate.PairSemantics.raw6481 line 307
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6481 line 309
  65. def OAI.MUB6.Certificate.PairSemantics.raw6482 line 313
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6482 line 315
  67. def OAI.MUB6.Certificate.PairSemantics.raw6483 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw6483step0 line 321
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6483 line 323
  70. def OAI.MUB6.Certificate.PairSemantics.raw6484 line 333
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6484 line 335
  72. def OAI.MUB6.Certificate.PairSemantics.raw6485 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw6485step0 line 341
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6485 line 343
  75. def OAI.MUB6.Certificate.PairSemantics.raw6486 line 352
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6486 line 354
  77. def OAI.MUB6.Certificate.PairSemantics.raw6487 line 358
  78. def OAI.MUB6.Certificate.PairSemantics.raw6487step0 line 360
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6487 line 362
  80. def OAI.MUB6.Certificate.PairSemantics.raw6488 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw6488step0 line 373
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6488 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw6489 line 384
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical6489 line 386
  85. def OAI.MUB6.Certificate.PairSemantics.raw6490 line 390
  86. def OAI.MUB6.Certificate.PairSemantics.raw6490step0 line 392
  87. def OAI.MUB6.Certificate.PairSemantics.raw6490step1 line 394
  88. def OAI.MUB6.Certificate.PairSemantics.raw6490step2 line 396
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6490 line 398
  90. def OAI.MUB6.Certificate.PairSemantics.raw6491 line 415
  91. def OAI.MUB6.Certificate.PairSemantics.raw6491step0 line 417
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical6491 line 419
  93. def OAI.MUB6.Certificate.PairSemantics.raw6492 line 428
  94. def OAI.MUB6.Certificate.PairSemantics.raw6492step0 line 430
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6492 line 432
  96. def OAI.MUB6.Certificate.PairSemantics.raw6493 line 441
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6493 line 443
  98. def OAI.MUB6.Certificate.PairSemantics.raw6494 line 447
  99. def OAI.MUB6.Certificate.PairSemantics.raw6494step0 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw6494step1 line 451
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical6494 line 453
  102. def OAI.MUB6.Certificate.PairSemantics.raw6495 line 466
  103. def OAI.MUB6.Certificate.PairSemantics.raw6495step0 line 468
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical6495 line 470