OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical59.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1888 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1888 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1889 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1889 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1890 line 28
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1890 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw1891 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1891 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw1892 line 40
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1892 line 42
  11. def OAI.MUB6.Certificate.PairSemantics.raw1893 line 46
  12. def OAI.MUB6.Certificate.PairSemantics.raw1893step0 line 48
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1893 line 50
  14. def OAI.MUB6.Certificate.PairSemantics.raw1894 line 59
  15. def OAI.MUB6.Certificate.PairSemantics.raw1894step0 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw1894step1 line 63
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1894 line 65
  18. def OAI.MUB6.Certificate.PairSemantics.raw1895 line 79
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1895 line 81
  20. def OAI.MUB6.Certificate.PairSemantics.raw1896 line 85
  21. def OAI.MUB6.Certificate.PairSemantics.raw1896step0 line 87
  22. def OAI.MUB6.Certificate.PairSemantics.raw1896step1 line 89
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1896 line 91
  24. def OAI.MUB6.Certificate.PairSemantics.raw1897 line 104
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1897 line 106
  26. def OAI.MUB6.Certificate.PairSemantics.raw1898 line 110
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1898 line 112
  28. def OAI.MUB6.Certificate.PairSemantics.raw1899 line 116
  29. def OAI.MUB6.Certificate.PairSemantics.raw1899step0 line 118
  30. def OAI.MUB6.Certificate.PairSemantics.raw1899step1 line 120
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1899 line 122
  32. def OAI.MUB6.Certificate.PairSemantics.raw1900 line 135
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1900 line 137
  34. def OAI.MUB6.Certificate.PairSemantics.raw1901 line 141
  35. def OAI.MUB6.Certificate.PairSemantics.raw1901step0 line 143
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1901 line 145
  37. def OAI.MUB6.Certificate.PairSemantics.raw1902 line 154
  38. def OAI.MUB6.Certificate.PairSemantics.raw1902step0 line 156
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1902 line 158
  40. def OAI.MUB6.Certificate.PairSemantics.raw1903 line 167
  41. def OAI.MUB6.Certificate.PairSemantics.raw1903step0 line 169
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1903 line 171
  43. def OAI.MUB6.Certificate.PairSemantics.raw1904 line 180
  44. def OAI.MUB6.Certificate.PairSemantics.raw1904step0 line 182
  45. def OAI.MUB6.Certificate.PairSemantics.raw1904step1 line 184
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1904 line 186
  47. def OAI.MUB6.Certificate.PairSemantics.raw1905 line 199
  48. def OAI.MUB6.Certificate.PairSemantics.raw1905step0 line 201
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1905 line 203
  50. def OAI.MUB6.Certificate.PairSemantics.raw1906 line 212
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1906 line 214
  52. def OAI.MUB6.Certificate.PairSemantics.raw1907 line 218
  53. def OAI.MUB6.Certificate.PairSemantics.raw1907step0 line 220
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical1907 line 222
  55. def OAI.MUB6.Certificate.PairSemantics.raw1908 line 231
  56. def OAI.MUB6.Certificate.PairSemantics.raw1908step0 line 233
  57. def OAI.MUB6.Certificate.PairSemantics.raw1908step1 line 235
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1908 line 237
  59. def OAI.MUB6.Certificate.PairSemantics.raw1909 line 250
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1909 line 252
  61. def OAI.MUB6.Certificate.PairSemantics.raw1910 line 256
  62. def OAI.MUB6.Certificate.PairSemantics.raw1910step0 line 258
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1910 line 260
  64. def OAI.MUB6.Certificate.PairSemantics.raw1911 line 269
  65. def OAI.MUB6.Certificate.PairSemantics.raw1911step0 line 271
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1911 line 273
  67. def OAI.MUB6.Certificate.PairSemantics.raw1912 line 282
  68. def OAI.MUB6.Certificate.PairSemantics.raw1912step0 line 284
  69. def OAI.MUB6.Certificate.PairSemantics.raw1912step1 line 286
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1912 line 288
  71. def OAI.MUB6.Certificate.PairSemantics.raw1913 line 301
  72. def OAI.MUB6.Certificate.PairSemantics.raw1913step0 line 303
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1913 line 305
  74. def OAI.MUB6.Certificate.PairSemantics.raw1914 line 314
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1914 line 316
  76. def OAI.MUB6.Certificate.PairSemantics.raw1915 line 320
  77. def OAI.MUB6.Certificate.PairSemantics.raw1915step0 line 322
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1915 line 324
  79. def OAI.MUB6.Certificate.PairSemantics.raw1916 line 333
  80. def OAI.MUB6.Certificate.PairSemantics.raw1916step0 line 335
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical1916 line 337
  82. def OAI.MUB6.Certificate.PairSemantics.raw1917 line 346
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1917 line 348
  84. def OAI.MUB6.Certificate.PairSemantics.raw1918 line 352
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1918 line 354
  86. def OAI.MUB6.Certificate.PairSemantics.raw1919 line 358
  87. def OAI.MUB6.Certificate.PairSemantics.raw1919step0 line 360
  88. def OAI.MUB6.Certificate.PairSemantics.raw1919step1 line 362
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1919 line 364