OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical151.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4832 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4832step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw4832step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4832 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw4833 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw4833step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw4833step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4833 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw4834 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw4834step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw4834step1 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4834 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw4835 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw4835step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw4835step1 line 81
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4835 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw4836 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw4836step0 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw4836step1 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4836 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw4837 line 115
  22. def OAI.MUB6.Certificate.PairSemantics.raw4837step0 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw4837step1 line 119
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4837 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw4838 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw4838step0 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw4838step1 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw4838step2 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4838 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw4839 line 159
  31. def OAI.MUB6.Certificate.PairSemantics.raw4839step0 line 161
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4839 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw4840 line 172
  34. def OAI.MUB6.Certificate.PairSemantics.raw4840step0 line 174
  35. def OAI.MUB6.Certificate.PairSemantics.raw4840step1 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw4840step2 line 178
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4840 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw4841 line 197
  39. def OAI.MUB6.Certificate.PairSemantics.raw4841step0 line 199
  40. def OAI.MUB6.Certificate.PairSemantics.raw4841step1 line 201
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical4841 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw4842 line 216
  43. def OAI.MUB6.Certificate.PairSemantics.raw4842step0 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw4842step1 line 220
  45. def OAI.MUB6.Certificate.PairSemantics.raw4842step2 line 222
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4842 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw4843 line 241
  48. def OAI.MUB6.Certificate.PairSemantics.raw4843step0 line 243
  49. def OAI.MUB6.Certificate.PairSemantics.raw4843step1 line 245
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4843 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw4844 line 260
  52. def OAI.MUB6.Certificate.PairSemantics.raw4844step0 line 262
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4844 line 264
  54. def OAI.MUB6.Certificate.PairSemantics.raw4845 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw4845step0 line 275
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4845 line 277
  57. def OAI.MUB6.Certificate.PairSemantics.raw4846 line 286
  58. def OAI.MUB6.Certificate.PairSemantics.raw4846step0 line 288
  59. def OAI.MUB6.Certificate.PairSemantics.raw4846step1 line 290
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical4846 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw4847 line 305
  62. def OAI.MUB6.Certificate.PairSemantics.raw4847step0 line 307
  63. def OAI.MUB6.Certificate.PairSemantics.raw4847step1 line 309
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4847 line 311
  65. def OAI.MUB6.Certificate.PairSemantics.raw4848 line 324
  66. def OAI.MUB6.Certificate.PairSemantics.raw4848step0 line 326
  67. def OAI.MUB6.Certificate.PairSemantics.raw4848step1 line 328
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical4848 line 330
  69. def OAI.MUB6.Certificate.PairSemantics.raw4849 line 343
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4849 line 345
  71. def OAI.MUB6.Certificate.PairSemantics.raw4850 line 349
  72. def OAI.MUB6.Certificate.PairSemantics.raw4850step0 line 351
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4850 line 353
  74. def OAI.MUB6.Certificate.PairSemantics.raw4851 line 362
  75. def OAI.MUB6.Certificate.PairSemantics.raw4851step0 line 364
  76. def OAI.MUB6.Certificate.PairSemantics.raw4851step1 line 366
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4851 line 368
  78. def OAI.MUB6.Certificate.PairSemantics.raw4852 line 381
  79. def OAI.MUB6.Certificate.PairSemantics.raw4852step0 line 383
  80. def OAI.MUB6.Certificate.PairSemantics.raw4852step1 line 385
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4852 line 387
  82. def OAI.MUB6.Certificate.PairSemantics.raw4853 line 400
  83. def OAI.MUB6.Certificate.PairSemantics.raw4853step0 line 402
  84. def OAI.MUB6.Certificate.PairSemantics.raw4853step1 line 404
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4853 line 406
  86. def OAI.MUB6.Certificate.PairSemantics.raw4854 line 419
  87. def OAI.MUB6.Certificate.PairSemantics.raw4854step0 line 421
  88. def OAI.MUB6.Certificate.PairSemantics.raw4854step1 line 423
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4854 line 425
  90. def OAI.MUB6.Certificate.PairSemantics.raw4855 line 438
  91. def OAI.MUB6.Certificate.PairSemantics.raw4855step0 line 440
  92. def OAI.MUB6.Certificate.PairSemantics.raw4855step1 line 442
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4855 line 444
  94. def OAI.MUB6.Certificate.PairSemantics.raw4856 line 457
  95. def OAI.MUB6.Certificate.PairSemantics.raw4856step0 line 459
  96. def OAI.MUB6.Certificate.PairSemantics.raw4856step1 line 461
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4856 line 463
  98. def OAI.MUB6.Certificate.PairSemantics.raw4857 line 476
  99. def OAI.MUB6.Certificate.PairSemantics.raw4857step0 line 478
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4857 line 480
  101. def OAI.MUB6.Certificate.PairSemantics.raw4858 line 489
  102. def OAI.MUB6.Certificate.PairSemantics.raw4858step0 line 491
  103. def OAI.MUB6.Certificate.PairSemantics.raw4858step1 line 493
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4858 line 495
  105. def OAI.MUB6.Certificate.PairSemantics.raw4859 line 508
  106. def OAI.MUB6.Certificate.PairSemantics.raw4859step0 line 510
  107. def OAI.MUB6.Certificate.PairSemantics.raw4859step1 line 512
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4859 line 514
  109. def OAI.MUB6.Certificate.PairSemantics.raw4860 line 527
  110. def OAI.MUB6.Certificate.PairSemantics.raw4860step0 line 529
  111. def OAI.MUB6.Certificate.PairSemantics.raw4860step1 line 531
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical4860 line 533
  113. def OAI.MUB6.Certificate.PairSemantics.raw4861 line 546
  114. def OAI.MUB6.Certificate.PairSemantics.raw4861step0 line 548
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical4861 line 550
  116. def OAI.MUB6.Certificate.PairSemantics.raw4862 line 559
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical4862 line 561
  118. def OAI.MUB6.Certificate.PairSemantics.raw4863 line 565
  119. def OAI.MUB6.Certificate.PairSemantics.raw4863step0 line 567
  120. def OAI.MUB6.Certificate.PairSemantics.raw4863step1 line 569
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical4863 line 571