OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical221.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7072 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical7072 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw7073 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7073 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw7074 line 28
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical7074 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw7075 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7075 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw7076 line 40
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7076 line 42
  11. def OAI.MUB6.Certificate.PairSemantics.raw7077 line 46
  12. def OAI.MUB6.Certificate.PairSemantics.raw7077step0 line 48
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7077 line 50
  14. def OAI.MUB6.Certificate.PairSemantics.raw7078 line 59
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7078 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw7079 line 65
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7079 line 67
  18. def OAI.MUB6.Certificate.PairSemantics.raw7080 line 71
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7080 line 73
  20. def OAI.MUB6.Certificate.PairSemantics.raw7081 line 77
  21. def OAI.MUB6.Certificate.PairSemantics.raw7081step0 line 79
  22. def OAI.MUB6.Certificate.PairSemantics.raw7081step1 line 81
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7081 line 83
  24. def OAI.MUB6.Certificate.PairSemantics.raw7082 line 96
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7082 line 98
  26. def OAI.MUB6.Certificate.PairSemantics.raw7083 line 102
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7083 line 104
  28. def OAI.MUB6.Certificate.PairSemantics.raw7084 line 108
  29. def OAI.MUB6.Certificate.PairSemantics.raw7084step0 line 110
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7084 line 112
  31. def OAI.MUB6.Certificate.PairSemantics.raw7085 line 121
  32. def OAI.MUB6.Certificate.PairSemantics.raw7085step0 line 123
  33. def OAI.MUB6.Certificate.PairSemantics.raw7085step1 line 125
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7085 line 127
  35. def OAI.MUB6.Certificate.PairSemantics.raw7086 line 140
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7086 line 142
  37. def OAI.MUB6.Certificate.PairSemantics.raw7087 line 146
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7087 line 148
  39. def OAI.MUB6.Certificate.PairSemantics.raw7088 line 152
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7088 line 154
  41. def OAI.MUB6.Certificate.PairSemantics.raw7089 line 158
  42. def OAI.MUB6.Certificate.PairSemantics.raw7089step0 line 160
  43. def OAI.MUB6.Certificate.PairSemantics.raw7089step1 line 162
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7089 line 164
  45. def OAI.MUB6.Certificate.PairSemantics.raw7090 line 177
  46. def OAI.MUB6.Certificate.PairSemantics.raw7090step0 line 179
  47. def OAI.MUB6.Certificate.PairSemantics.raw7090step1 line 181
  48. def OAI.MUB6.Certificate.PairSemantics.raw7090step2 line 183
  49. def OAI.MUB6.Certificate.PairSemantics.raw7090step3 line 185
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7090 line 187
  51. def OAI.MUB6.Certificate.PairSemantics.raw7091 line 210
  52. def OAI.MUB6.Certificate.PairSemantics.raw7091step0 line 212
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical7091 line 214
  54. def OAI.MUB6.Certificate.PairSemantics.raw7092 line 223
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7092 line 225
  56. def OAI.MUB6.Certificate.PairSemantics.raw7093 line 229
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7093 line 231
  58. def OAI.MUB6.Certificate.PairSemantics.raw7094 line 235
  59. def OAI.MUB6.Certificate.PairSemantics.raw7094step0 line 237
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical7094 line 239
  61. def OAI.MUB6.Certificate.PairSemantics.raw7095 line 249
  62. def OAI.MUB6.Certificate.PairSemantics.raw7095step0 line 251
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical7095 line 253
  64. def OAI.MUB6.Certificate.PairSemantics.raw7096 line 263
  65. def OAI.MUB6.Certificate.PairSemantics.raw7096step0 line 265
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7096 line 267
  67. def OAI.MUB6.Certificate.PairSemantics.raw7097 line 276
  68. def OAI.MUB6.Certificate.PairSemantics.raw7097step0 line 278
  69. def OAI.MUB6.Certificate.PairSemantics.raw7097step1 line 280
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7097 line 282
  71. def OAI.MUB6.Certificate.PairSemantics.raw7098 line 295
  72. def OAI.MUB6.Certificate.PairSemantics.raw7098step0 line 297
  73. def OAI.MUB6.Certificate.PairSemantics.raw7098step1 line 299
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7098 line 301
  75. def OAI.MUB6.Certificate.PairSemantics.raw7099 line 314
  76. def OAI.MUB6.Certificate.PairSemantics.raw7099step0 line 316
  77. def OAI.MUB6.Certificate.PairSemantics.raw7099step1 line 318
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7099 line 320
  79. def OAI.MUB6.Certificate.PairSemantics.raw7100 line 333
  80. def OAI.MUB6.Certificate.PairSemantics.raw7100step0 line 335
  81. def OAI.MUB6.Certificate.PairSemantics.raw7100step1 line 337
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7100 line 339
  83. def OAI.MUB6.Certificate.PairSemantics.raw7101 line 352
  84. def OAI.MUB6.Certificate.PairSemantics.raw7101step0 line 354
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7101 line 356
  86. def OAI.MUB6.Certificate.PairSemantics.raw7102 line 366
  87. def OAI.MUB6.Certificate.PairSemantics.raw7102step0 line 368
  88. def OAI.MUB6.Certificate.PairSemantics.raw7102step1 line 370
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7102 line 372
  90. def OAI.MUB6.Certificate.PairSemantics.raw7103 line 387
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7103 line 389