OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical25.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw800 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical800 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw801 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical801 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw802 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw802step0 line 27
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical802 line 29
  8. def OAI.MUB6.Certificate.PairSemantics.raw803 line 38
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical803 line 40
  10. def OAI.MUB6.Certificate.PairSemantics.raw804 line 44
  11. def OAI.MUB6.Certificate.PairSemantics.raw804step0 line 46
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical804 line 48
  13. def OAI.MUB6.Certificate.PairSemantics.raw805 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw805step0 line 59
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical805 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw806 line 70
  17. def OAI.MUB6.Certificate.PairSemantics.raw806step0 line 72
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical806 line 74
  19. def OAI.MUB6.Certificate.PairSemantics.raw807 line 83
  20. def OAI.MUB6.Certificate.PairSemantics.raw807step0 line 85
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical807 line 87
  22. def OAI.MUB6.Certificate.PairSemantics.raw808 line 96
  23. def OAI.MUB6.Certificate.PairSemantics.raw808step0 line 98
  24. def OAI.MUB6.Certificate.PairSemantics.raw808step1 line 100
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical808 line 102
  26. def OAI.MUB6.Certificate.PairSemantics.raw809 line 115
  27. def OAI.MUB6.Certificate.PairSemantics.raw809step0 line 117
  28. def OAI.MUB6.Certificate.PairSemantics.raw809step1 line 119
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical809 line 121
  30. def OAI.MUB6.Certificate.PairSemantics.raw810 line 134
  31. def OAI.MUB6.Certificate.PairSemantics.raw810step0 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw810step1 line 138
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical810 line 140
  34. def OAI.MUB6.Certificate.PairSemantics.raw811 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw811step0 line 155
  36. def OAI.MUB6.Certificate.PairSemantics.raw811step1 line 157
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical811 line 159
  38. def OAI.MUB6.Certificate.PairSemantics.raw812 line 172
  39. def OAI.MUB6.Certificate.PairSemantics.raw812step0 line 174
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical812 line 176
  41. def OAI.MUB6.Certificate.PairSemantics.raw813 line 185
  42. def OAI.MUB6.Certificate.PairSemantics.raw813step0 line 187
  43. def OAI.MUB6.Certificate.PairSemantics.raw813step1 line 189
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical813 line 191
  45. def OAI.MUB6.Certificate.PairSemantics.raw814 line 204
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical814 line 206
  47. def OAI.MUB6.Certificate.PairSemantics.raw815 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw815step0 line 212
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical815 line 214
  50. def OAI.MUB6.Certificate.PairSemantics.raw816 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw816step0 line 225
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical816 line 227
  53. def OAI.MUB6.Certificate.PairSemantics.raw817 line 236
  54. def OAI.MUB6.Certificate.PairSemantics.raw817step0 line 238
  55. def OAI.MUB6.Certificate.PairSemantics.raw817step1 line 240
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical817 line 242
  57. def OAI.MUB6.Certificate.PairSemantics.raw818 line 255
  58. def OAI.MUB6.Certificate.PairSemantics.raw818step0 line 257
  59. def OAI.MUB6.Certificate.PairSemantics.raw818step1 line 259
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical818 line 261
  61. def OAI.MUB6.Certificate.PairSemantics.raw819 line 274
  62. def OAI.MUB6.Certificate.PairSemantics.raw819step0 line 276
  63. def OAI.MUB6.Certificate.PairSemantics.raw819step1 line 278
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical819 line 280
  65. def OAI.MUB6.Certificate.PairSemantics.raw820 line 293
  66. def OAI.MUB6.Certificate.PairSemantics.raw820step0 line 295
  67. def OAI.MUB6.Certificate.PairSemantics.raw820step1 line 297
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical820 line 299
  69. def OAI.MUB6.Certificate.PairSemantics.raw821 line 312
  70. def OAI.MUB6.Certificate.PairSemantics.raw821step0 line 314
  71. def OAI.MUB6.Certificate.PairSemantics.raw821step1 line 316
  72. def OAI.MUB6.Certificate.PairSemantics.raw821step2 line 318
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical821 line 320
  74. def OAI.MUB6.Certificate.PairSemantics.raw822 line 337
  75. def OAI.MUB6.Certificate.PairSemantics.raw822step0 line 339
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical822 line 341
  77. def OAI.MUB6.Certificate.PairSemantics.raw823 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw823step0 line 352
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical823 line 354
  80. def OAI.MUB6.Certificate.PairSemantics.raw824 line 363
  81. def OAI.MUB6.Certificate.PairSemantics.raw824step0 line 365
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical824 line 367
  83. def OAI.MUB6.Certificate.PairSemantics.raw825 line 376
  84. def OAI.MUB6.Certificate.PairSemantics.raw825step0 line 378
  85. def OAI.MUB6.Certificate.PairSemantics.raw825step1 line 380
  86. def OAI.MUB6.Certificate.PairSemantics.raw825step2 line 382
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical825 line 384
  88. def OAI.MUB6.Certificate.PairSemantics.raw826 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw826step0 line 404
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical826 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw827 line 415
  92. def OAI.MUB6.Certificate.PairSemantics.raw827step0 line 417
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical827 line 419
  94. def OAI.MUB6.Certificate.PairSemantics.raw828 line 428
  95. def OAI.MUB6.Certificate.PairSemantics.raw828step0 line 430
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical828 line 432
  97. def OAI.MUB6.Certificate.PairSemantics.raw829 line 441
  98. def OAI.MUB6.Certificate.PairSemantics.raw829step0 line 443
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical829 line 445
  100. def OAI.MUB6.Certificate.PairSemantics.raw830 line 454
  101. def OAI.MUB6.Certificate.PairSemantics.raw830step0 line 456
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical830 line 458
  103. def OAI.MUB6.Certificate.PairSemantics.raw831 line 467
  104. def OAI.MUB6.Certificate.PairSemantics.raw831step0 line 469
  105. def OAI.MUB6.Certificate.PairSemantics.raw831step1 line 471
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical831 line 473