OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical115.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3680 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw3680step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw3680step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3680 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw3681 line 38
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical3681 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw3682 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw3682step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3682 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw3683 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3683 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw3684 line 63
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3684 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw3685 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3685 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw3686 line 75
  17. def OAI.MUB6.Certificate.PairSemantics.raw3686step0 line 77
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3686 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw3687 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw3687step0 line 90
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3687 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw3688 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw3688step0 line 103
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3688 line 105
  25. def OAI.MUB6.Certificate.PairSemantics.raw3689 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw3689step0 line 116
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3689 line 118
  28. def OAI.MUB6.Certificate.PairSemantics.raw3690 line 127
  29. def OAI.MUB6.Certificate.PairSemantics.raw3690step0 line 129
  30. def OAI.MUB6.Certificate.PairSemantics.raw3690step1 line 131
  31. def OAI.MUB6.Certificate.PairSemantics.raw3690step2 line 133
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3690 line 135
  33. def OAI.MUB6.Certificate.PairSemantics.raw3691 line 152
  34. def OAI.MUB6.Certificate.PairSemantics.raw3691step0 line 154
  35. def OAI.MUB6.Certificate.PairSemantics.raw3691step1 line 156
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3691 line 158
  37. def OAI.MUB6.Certificate.PairSemantics.raw3692 line 171
  38. def OAI.MUB6.Certificate.PairSemantics.raw3692step0 line 173
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3692 line 175
  40. def OAI.MUB6.Certificate.PairSemantics.raw3693 line 184
  41. def OAI.MUB6.Certificate.PairSemantics.raw3693step0 line 186
  42. def OAI.MUB6.Certificate.PairSemantics.raw3693step1 line 188
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3693 line 190
  44. def OAI.MUB6.Certificate.PairSemantics.raw3694 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw3694step0 line 205
  46. def OAI.MUB6.Certificate.PairSemantics.raw3694step1 line 207
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3694 line 209
  48. def OAI.MUB6.Certificate.PairSemantics.raw3695 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw3695step0 line 224
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3695 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw3696 line 235
  52. def OAI.MUB6.Certificate.PairSemantics.raw3696step0 line 237
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3696 line 239
  54. def OAI.MUB6.Certificate.PairSemantics.raw3697 line 248
  55. def OAI.MUB6.Certificate.PairSemantics.raw3697step0 line 250
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3697 line 252
  57. def OAI.MUB6.Certificate.PairSemantics.raw3698 line 261
  58. def OAI.MUB6.Certificate.PairSemantics.raw3698step0 line 263
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3698 line 265
  60. def OAI.MUB6.Certificate.PairSemantics.raw3699 line 274
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3699 line 276
  62. def OAI.MUB6.Certificate.PairSemantics.raw3700 line 280
  63. def OAI.MUB6.Certificate.PairSemantics.raw3700step0 line 282
  64. def OAI.MUB6.Certificate.PairSemantics.raw3700step1 line 284
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3700 line 286
  66. def OAI.MUB6.Certificate.PairSemantics.raw3701 line 299
  67. def OAI.MUB6.Certificate.PairSemantics.raw3701step0 line 301
  68. def OAI.MUB6.Certificate.PairSemantics.raw3701step1 line 303
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3701 line 305
  70. def OAI.MUB6.Certificate.PairSemantics.raw3702 line 318
  71. def OAI.MUB6.Certificate.PairSemantics.raw3702step0 line 320
  72. def OAI.MUB6.Certificate.PairSemantics.raw3702step1 line 322
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3702 line 324
  74. def OAI.MUB6.Certificate.PairSemantics.raw3703 line 337
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3703 line 339
  76. def OAI.MUB6.Certificate.PairSemantics.raw3704 line 343
  77. def OAI.MUB6.Certificate.PairSemantics.raw3704step0 line 345
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical3704 line 347
  79. def OAI.MUB6.Certificate.PairSemantics.raw3705 line 356
  80. def OAI.MUB6.Certificate.PairSemantics.raw3705step0 line 358
  81. def OAI.MUB6.Certificate.PairSemantics.raw3705step1 line 360
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3705 line 362
  83. def OAI.MUB6.Certificate.PairSemantics.raw3706 line 375
  84. def OAI.MUB6.Certificate.PairSemantics.raw3706step0 line 377
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3706 line 379
  86. def OAI.MUB6.Certificate.PairSemantics.raw3707 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw3707step0 line 390
  88. def OAI.MUB6.Certificate.PairSemantics.raw3707step1 line 392
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3707 line 394
  90. def OAI.MUB6.Certificate.PairSemantics.raw3708 line 407
  91. def OAI.MUB6.Certificate.PairSemantics.raw3708step0 line 409
  92. def OAI.MUB6.Certificate.PairSemantics.raw3708step1 line 411
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3708 line 413
  94. def OAI.MUB6.Certificate.PairSemantics.raw3709 line 426
  95. def OAI.MUB6.Certificate.PairSemantics.raw3709step0 line 428
  96. def OAI.MUB6.Certificate.PairSemantics.raw3709step1 line 430
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical3709 line 432
  98. def OAI.MUB6.Certificate.PairSemantics.raw3710 line 445
  99. def OAI.MUB6.Certificate.PairSemantics.raw3710step0 line 447
  100. def OAI.MUB6.Certificate.PairSemantics.raw3710step1 line 449
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3710 line 451
  102. def OAI.MUB6.Certificate.PairSemantics.raw3711 line 464
  103. def OAI.MUB6.Certificate.PairSemantics.raw3711step0 line 466
  104. def OAI.MUB6.Certificate.PairSemantics.raw3711step1 line 468
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3711 line 470