OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical214.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6848 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw6848step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6848 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw6849 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw6849step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6849 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw6850 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw6850step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6850 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw6851 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw6851step0 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6851 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw6852 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6852 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw6853 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw6853step0 line 75
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6853 line 77
  18. def OAI.MUB6.Certificate.PairSemantics.raw6854 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw6854step0 line 89
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6854 line 91
  21. def OAI.MUB6.Certificate.PairSemantics.raw6855 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw6855step0 line 102
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical6855 line 104
  24. def OAI.MUB6.Certificate.PairSemantics.raw6856 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw6856step0 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6856 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw6857 line 126
  28. def OAI.MUB6.Certificate.PairSemantics.raw6857step0 line 128
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6857 line 130
  30. def OAI.MUB6.Certificate.PairSemantics.raw6858 line 139
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6858 line 141
  32. def OAI.MUB6.Certificate.PairSemantics.raw6859 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw6859step0 line 147
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6859 line 149
  35. def OAI.MUB6.Certificate.PairSemantics.raw6860 line 158
  36. def OAI.MUB6.Certificate.PairSemantics.raw6860step0 line 160
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6860 line 162
  38. def OAI.MUB6.Certificate.PairSemantics.raw6861 line 171
  39. def OAI.MUB6.Certificate.PairSemantics.raw6861step0 line 173
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6861 line 175
  41. def OAI.MUB6.Certificate.PairSemantics.raw6862 line 184
  42. def OAI.MUB6.Certificate.PairSemantics.raw6862step0 line 186
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6862 line 188
  44. def OAI.MUB6.Certificate.PairSemantics.raw6863 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw6863step0 line 199
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6863 line 201
  47. def OAI.MUB6.Certificate.PairSemantics.raw6864 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw6864step0 line 212
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6864 line 214
  50. def OAI.MUB6.Certificate.PairSemantics.raw6865 line 223
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6865 line 225
  52. def OAI.MUB6.Certificate.PairSemantics.raw6866 line 229
  53. def OAI.MUB6.Certificate.PairSemantics.raw6866step0 line 231
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6866 line 233
  55. def OAI.MUB6.Certificate.PairSemantics.raw6867 line 242
  56. def OAI.MUB6.Certificate.PairSemantics.raw6867step0 line 244
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6867 line 246
  58. def OAI.MUB6.Certificate.PairSemantics.raw6868 line 255
  59. def OAI.MUB6.Certificate.PairSemantics.raw6868step0 line 257
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6868 line 259
  61. def OAI.MUB6.Certificate.PairSemantics.raw6869 line 268
  62. def OAI.MUB6.Certificate.PairSemantics.raw6869step0 line 270
  63. def OAI.MUB6.Certificate.PairSemantics.raw6869step1 line 272
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6869 line 274
  65. def OAI.MUB6.Certificate.PairSemantics.raw6870 line 287
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6870 line 289
  67. def OAI.MUB6.Certificate.PairSemantics.raw6871 line 293
  68. def OAI.MUB6.Certificate.PairSemantics.raw6871step0 line 295
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6871 line 297
  70. def OAI.MUB6.Certificate.PairSemantics.raw6872 line 307
  71. def OAI.MUB6.Certificate.PairSemantics.raw6872step0 line 309
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6872 line 311
  73. def OAI.MUB6.Certificate.PairSemantics.raw6873 line 320
  74. def OAI.MUB6.Certificate.PairSemantics.raw6873step0 line 322
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6873 line 324
  76. def OAI.MUB6.Certificate.PairSemantics.raw6874 line 333
  77. def OAI.MUB6.Certificate.PairSemantics.raw6874step0 line 335
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6874 line 337
  79. def OAI.MUB6.Certificate.PairSemantics.raw6875 line 346
  80. def OAI.MUB6.Certificate.PairSemantics.raw6875step0 line 348
  81. def OAI.MUB6.Certificate.PairSemantics.raw6875step1 line 350
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6875 line 352
  83. def OAI.MUB6.Certificate.PairSemantics.raw6876 line 365
  84. def OAI.MUB6.Certificate.PairSemantics.raw6876step0 line 367
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6876 line 369
  86. def OAI.MUB6.Certificate.PairSemantics.raw6877 line 378
  87. def OAI.MUB6.Certificate.PairSemantics.raw6877step0 line 380
  88. def OAI.MUB6.Certificate.PairSemantics.raw6877step1 line 382
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6877 line 384
  90. def OAI.MUB6.Certificate.PairSemantics.raw6878 line 397
  91. def OAI.MUB6.Certificate.PairSemantics.raw6878step0 line 399
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical6878 line 401
  93. def OAI.MUB6.Certificate.PairSemantics.raw6879 line 410
  94. def OAI.MUB6.Certificate.PairSemantics.raw6879step0 line 412
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6879 line 414