OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical28.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw896 line 9
  2. def OAI.MUB6.Certificate.PairSemantics.raw896step0 line 11
  3. def OAI.MUB6.Certificate.PairSemantics.raw896step1 line 13
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical896 line 15
  5. def OAI.MUB6.Certificate.PairSemantics.raw897 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw897step0 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw897step1 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw897step2 line 36
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical897 line 38
  10. def OAI.MUB6.Certificate.PairSemantics.raw898 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw898step0 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw898step1 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical898 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw899 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw899step0 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw899step1 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw899step2 line 83
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical899 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw900 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw900step0 line 106
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical900 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw901 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw901step0 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw901step1 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical901 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw902 line 139
  27. def OAI.MUB6.Certificate.PairSemantics.raw902step0 line 141
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical902 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw903 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw903step0 line 154
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical903 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw904 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw904step0 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw904step1 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw904step2 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical904 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw905 line 193
  38. def OAI.MUB6.Certificate.PairSemantics.raw905step0 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw905step1 line 197
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical905 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw906 line 214
  42. def OAI.MUB6.Certificate.PairSemantics.raw906step0 line 216
  43. def OAI.MUB6.Certificate.PairSemantics.raw906step1 line 218
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical906 line 220
  45. def OAI.MUB6.Certificate.PairSemantics.raw907 line 235
  46. def OAI.MUB6.Certificate.PairSemantics.raw907step0 line 237
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical907 line 239
  48. def OAI.MUB6.Certificate.PairSemantics.raw908 line 249
  49. def OAI.MUB6.Certificate.PairSemantics.raw908step0 line 251
  50. def OAI.MUB6.Certificate.PairSemantics.raw908step1 line 253
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical908 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw909 line 270
  53. def OAI.MUB6.Certificate.PairSemantics.raw909step0 line 272
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical909 line 274
  55. def OAI.MUB6.Certificate.PairSemantics.raw910 line 284
  56. def OAI.MUB6.Certificate.PairSemantics.raw910step0 line 286
  57. def OAI.MUB6.Certificate.PairSemantics.raw910step1 line 288
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical910 line 290
  59. def OAI.MUB6.Certificate.PairSemantics.raw911 line 305
  60. def OAI.MUB6.Certificate.PairSemantics.raw911step0 line 307
  61. def OAI.MUB6.Certificate.PairSemantics.raw911step1 line 309
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical911 line 311
  63. def OAI.MUB6.Certificate.PairSemantics.raw912 line 326
  64. def OAI.MUB6.Certificate.PairSemantics.raw912step0 line 328
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical912 line 330
  66. def OAI.MUB6.Certificate.PairSemantics.raw913 line 340
  67. def OAI.MUB6.Certificate.PairSemantics.raw913step0 line 342
  68. def OAI.MUB6.Certificate.PairSemantics.raw913step1 line 344
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical913 line 346
  70. def OAI.MUB6.Certificate.PairSemantics.raw914 line 361
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical914 line 363
  72. def OAI.MUB6.Certificate.PairSemantics.raw915 line 367
  73. def OAI.MUB6.Certificate.PairSemantics.raw915step0 line 369
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical915 line 371
  75. def OAI.MUB6.Certificate.PairSemantics.raw916 line 381
  76. def OAI.MUB6.Certificate.PairSemantics.raw916step0 line 383
  77. def OAI.MUB6.Certificate.PairSemantics.raw916step1 line 385
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical916 line 387
  79. def OAI.MUB6.Certificate.PairSemantics.raw917 line 402
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical917 line 404
  81. def OAI.MUB6.Certificate.PairSemantics.raw918 line 408
  82. def OAI.MUB6.Certificate.PairSemantics.raw918step0 line 410
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical918 line 412
  84. def OAI.MUB6.Certificate.PairSemantics.raw919 line 422
  85. def OAI.MUB6.Certificate.PairSemantics.raw919step0 line 424
  86. def OAI.MUB6.Certificate.PairSemantics.raw919step1 line 426
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical919 line 428
  88. def OAI.MUB6.Certificate.PairSemantics.raw920 line 443
  89. def OAI.MUB6.Certificate.PairSemantics.raw920step0 line 445
  90. def OAI.MUB6.Certificate.PairSemantics.raw920step1 line 447
  91. def OAI.MUB6.Certificate.PairSemantics.raw920step2 line 449
  92. def OAI.MUB6.Certificate.PairSemantics.raw920step3 line 451
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical920 line 453
  94. def OAI.MUB6.Certificate.PairSemantics.raw921 line 477
  95. def OAI.MUB6.Certificate.PairSemantics.raw921step0 line 479
  96. def OAI.MUB6.Certificate.PairSemantics.raw921step1 line 481
  97. def OAI.MUB6.Certificate.PairSemantics.raw921step2 line 483
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical921 line 485
  99. def OAI.MUB6.Certificate.PairSemantics.raw922 line 504
  100. def OAI.MUB6.Certificate.PairSemantics.raw922step0 line 506
  101. def OAI.MUB6.Certificate.PairSemantics.raw922step1 line 508
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical922 line 510
  103. def OAI.MUB6.Certificate.PairSemantics.raw923 line 524
  104. def OAI.MUB6.Certificate.PairSemantics.raw923step0 line 526
  105. def OAI.MUB6.Certificate.PairSemantics.raw923step1 line 528
  106. def OAI.MUB6.Certificate.PairSemantics.raw923step2 line 530
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical923 line 532
  108. def OAI.MUB6.Certificate.PairSemantics.raw924 line 551
  109. def OAI.MUB6.Certificate.PairSemantics.raw924step0 line 553
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical924 line 555
  111. def OAI.MUB6.Certificate.PairSemantics.raw925 line 564
  112. def OAI.MUB6.Certificate.PairSemantics.raw925step0 line 566
  113. def OAI.MUB6.Certificate.PairSemantics.raw925step1 line 568
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical925 line 570
  115. def OAI.MUB6.Certificate.PairSemantics.raw926 line 584
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical926 line 586
  117. def OAI.MUB6.Certificate.PairSemantics.raw927 line 590
  118. def OAI.MUB6.Certificate.PairSemantics.raw927step0 line 592
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical927 line 594