OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical122.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3904 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw3904step0 line 25
  3. def OAI.MUB6.Certificate.PairSemantics.raw3904step1 line 27
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3904 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw3905 line 42
  6. def OAI.MUB6.Certificate.PairSemantics.raw3905step0 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw3905step1 line 46
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3905 line 48
  9. def OAI.MUB6.Certificate.PairSemantics.raw3906 line 61
  10. def OAI.MUB6.Certificate.PairSemantics.raw3906step0 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw3906step1 line 65
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3906 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw3907 line 80
  14. def OAI.MUB6.Certificate.PairSemantics.raw3907step0 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw3907step1 line 84
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3907 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw3908 line 99
  18. def OAI.MUB6.Certificate.PairSemantics.raw3908step0 line 101
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3908 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw3909 line 112
  21. def OAI.MUB6.Certificate.PairSemantics.raw3909step0 line 114
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3909 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw3910 line 125
  24. def OAI.MUB6.Certificate.PairSemantics.raw3910step0 line 127
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3910 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw3911 line 138
  27. def OAI.MUB6.Certificate.PairSemantics.raw3911step0 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw3911step1 line 142
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3911 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw3912 line 157
  31. def OAI.MUB6.Certificate.PairSemantics.raw3912step0 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw3912step1 line 161
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3912 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw3913 line 176
  35. def OAI.MUB6.Certificate.PairSemantics.raw3913step0 line 178
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3913 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw3914 line 189
  38. def OAI.MUB6.Certificate.PairSemantics.raw3914step0 line 191
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3914 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw3915 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw3915step0 line 204
  42. def OAI.MUB6.Certificate.PairSemantics.raw3915step1 line 206
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3915 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw3916 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw3916step0 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw3916step1 line 225
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3916 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw3917 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw3917step0 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw3917step1 line 244
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3917 line 246
  52. def OAI.MUB6.Certificate.PairSemantics.raw3918 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw3918step0 line 261
  54. def OAI.MUB6.Certificate.PairSemantics.raw3918step1 line 263
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3918 line 265
  56. def OAI.MUB6.Certificate.PairSemantics.raw3919 line 280
  57. def OAI.MUB6.Certificate.PairSemantics.raw3919step0 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw3919step1 line 284
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3919 line 286
  60. def OAI.MUB6.Certificate.PairSemantics.raw3920 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw3920step0 line 302
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3920 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw3921 line 313
  64. def OAI.MUB6.Certificate.PairSemantics.raw3921step0 line 315
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3921 line 317
  66. def OAI.MUB6.Certificate.PairSemantics.raw3922 line 326
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical3922 line 328
  68. def OAI.MUB6.Certificate.PairSemantics.raw3923 line 332
  69. def OAI.MUB6.Certificate.PairSemantics.raw3923step0 line 334
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3923 line 336
  71. def OAI.MUB6.Certificate.PairSemantics.raw3924 line 345
  72. def OAI.MUB6.Certificate.PairSemantics.raw3924step0 line 347
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3924 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw3925 line 358
  75. def OAI.MUB6.Certificate.PairSemantics.raw3925step0 line 360
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3925 line 362
  77. def OAI.MUB6.Certificate.PairSemantics.raw3926 line 371
  78. def OAI.MUB6.Certificate.PairSemantics.raw3926step0 line 373
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3926 line 375
  80. def OAI.MUB6.Certificate.PairSemantics.raw3927 line 384
  81. def OAI.MUB6.Certificate.PairSemantics.raw3927step0 line 386
  82. def OAI.MUB6.Certificate.PairSemantics.raw3927step1 line 388
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3927 line 390
  84. def OAI.MUB6.Certificate.PairSemantics.raw3928 line 403
  85. def OAI.MUB6.Certificate.PairSemantics.raw3928step0 line 405
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3928 line 407
  87. def OAI.MUB6.Certificate.PairSemantics.raw3929 line 416
  88. def OAI.MUB6.Certificate.PairSemantics.raw3929step0 line 418
  89. def OAI.MUB6.Certificate.PairSemantics.raw3929step1 line 420
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3929 line 422
  91. def OAI.MUB6.Certificate.PairSemantics.raw3930 line 435
  92. def OAI.MUB6.Certificate.PairSemantics.raw3930step0 line 437
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3930 line 439
  94. def OAI.MUB6.Certificate.PairSemantics.raw3931 line 449
  95. def OAI.MUB6.Certificate.PairSemantics.raw3931step0 line 451
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3931 line 453
  97. def OAI.MUB6.Certificate.PairSemantics.raw3932 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw3932step0 line 464
  99. def OAI.MUB6.Certificate.PairSemantics.raw3932step1 line 466
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3932 line 468
  101. def OAI.MUB6.Certificate.PairSemantics.raw3933 line 481
  102. def OAI.MUB6.Certificate.PairSemantics.raw3933step0 line 483
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3933 line 485
  104. def OAI.MUB6.Certificate.PairSemantics.raw3934 line 494
  105. def OAI.MUB6.Certificate.PairSemantics.raw3934step0 line 496
  106. def OAI.MUB6.Certificate.PairSemantics.raw3934step1 line 498
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3934 line 500
  108. def OAI.MUB6.Certificate.PairSemantics.raw3935 line 513
  109. def OAI.MUB6.Certificate.PairSemantics.raw3935step0 line 515
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical3935 line 517