OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical60.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1920 line 17
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1920 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw1921 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw1921step0 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw1921step1 line 27
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1921 line 29
  7. def OAI.MUB6.Certificate.PairSemantics.raw1922 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1922 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw1923 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw1923step0 line 50
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1923 line 52
  12. def OAI.MUB6.Certificate.PairSemantics.raw1924 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw1924step0 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw1924step1 line 65
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1924 line 67
  16. def OAI.MUB6.Certificate.PairSemantics.raw1925 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw1925step0 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1925 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw1926 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw1926step0 line 95
  21. def OAI.MUB6.Certificate.PairSemantics.raw1926step1 line 97
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1926 line 99
  23. def OAI.MUB6.Certificate.PairSemantics.raw1927 line 112
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1927 line 114
  25. def OAI.MUB6.Certificate.PairSemantics.raw1928 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw1928step0 line 120
  27. def OAI.MUB6.Certificate.PairSemantics.raw1928step1 line 122
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1928 line 124
  29. def OAI.MUB6.Certificate.PairSemantics.raw1929 line 137
  30. def OAI.MUB6.Certificate.PairSemantics.raw1929step0 line 139
  31. def OAI.MUB6.Certificate.PairSemantics.raw1929step1 line 141
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1929 line 143
  33. def OAI.MUB6.Certificate.PairSemantics.raw1930 line 156
  34. def OAI.MUB6.Certificate.PairSemantics.raw1930step0 line 158
  35. def OAI.MUB6.Certificate.PairSemantics.raw1930step1 line 160
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1930 line 162
  37. def OAI.MUB6.Certificate.PairSemantics.raw1931 line 175
  38. def OAI.MUB6.Certificate.PairSemantics.raw1931step0 line 177
  39. def OAI.MUB6.Certificate.PairSemantics.raw1931step1 line 179
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1931 line 181
  41. def OAI.MUB6.Certificate.PairSemantics.raw1932 line 194
  42. def OAI.MUB6.Certificate.PairSemantics.raw1932step0 line 196
  43. def OAI.MUB6.Certificate.PairSemantics.raw1932step1 line 198
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1932 line 200
  45. def OAI.MUB6.Certificate.PairSemantics.raw1933 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw1933step0 line 215
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1933 line 217
  48. def OAI.MUB6.Certificate.PairSemantics.raw1934 line 226
  49. def OAI.MUB6.Certificate.PairSemantics.raw1934step0 line 228
  50. def OAI.MUB6.Certificate.PairSemantics.raw1934step1 line 230
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1934 line 232
  52. def OAI.MUB6.Certificate.PairSemantics.raw1935 line 245
  53. def OAI.MUB6.Certificate.PairSemantics.raw1935step0 line 247
  54. def OAI.MUB6.Certificate.PairSemantics.raw1935step1 line 249
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1935 line 251
  56. def OAI.MUB6.Certificate.PairSemantics.raw1936 line 264
  57. def OAI.MUB6.Certificate.PairSemantics.raw1936step0 line 266
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1936 line 268
  59. def OAI.MUB6.Certificate.PairSemantics.raw1937 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw1937step0 line 279
  61. def OAI.MUB6.Certificate.PairSemantics.raw1937step1 line 281
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1937 line 283
  63. def OAI.MUB6.Certificate.PairSemantics.raw1938 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw1938step0 line 298
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1938 line 300
  66. def OAI.MUB6.Certificate.PairSemantics.raw1939 line 309
  67. def OAI.MUB6.Certificate.PairSemantics.raw1939step0 line 311
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1939 line 313
  69. def OAI.MUB6.Certificate.PairSemantics.raw1940 line 322
  70. def OAI.MUB6.Certificate.PairSemantics.raw1940step0 line 324
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1940 line 326
  72. def OAI.MUB6.Certificate.PairSemantics.raw1941 line 335
  73. def OAI.MUB6.Certificate.PairSemantics.raw1941step0 line 337
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1941 line 339
  75. def OAI.MUB6.Certificate.PairSemantics.raw1942 line 348
  76. def OAI.MUB6.Certificate.PairSemantics.raw1942step0 line 350
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1942 line 352
  78. def OAI.MUB6.Certificate.PairSemantics.raw1943 line 361
  79. def OAI.MUB6.Certificate.PairSemantics.raw1943step0 line 363
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1943 line 365
  81. def OAI.MUB6.Certificate.PairSemantics.raw1944 line 374
  82. def OAI.MUB6.Certificate.PairSemantics.raw1944step0 line 376
  83. def OAI.MUB6.Certificate.PairSemantics.raw1944step1 line 378
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical1944 line 380
  85. def OAI.MUB6.Certificate.PairSemantics.raw1945 line 394
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1945 line 396
  87. def OAI.MUB6.Certificate.PairSemantics.raw1946 line 400
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical1946 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw1947 line 406
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1947 line 408
  91. def OAI.MUB6.Certificate.PairSemantics.raw1948 line 412
  92. def OAI.MUB6.Certificate.PairSemantics.raw1948step0 line 414
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1948 line 416
  94. def OAI.MUB6.Certificate.PairSemantics.raw1949 line 425
  95. def OAI.MUB6.Certificate.PairSemantics.raw1949step0 line 427
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1949 line 429
  97. def OAI.MUB6.Certificate.PairSemantics.raw1950 line 438
  98. def OAI.MUB6.Certificate.PairSemantics.raw1950step0 line 440
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical1950 line 442
  100. def OAI.MUB6.Certificate.PairSemantics.raw1951 line 451
  101. def OAI.MUB6.Certificate.PairSemantics.raw1951step0 line 453
  102. def OAI.MUB6.Certificate.PairSemantics.raw1951step1 line 455
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical1951 line 457