OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical34.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1088 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw1088step0 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw1088step1 line 16
  4. def OAI.MUB6.Certificate.PairSemantics.raw1088step2 line 18
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1088 line 20
  6. def OAI.MUB6.Certificate.PairSemantics.raw1089 line 37
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1089 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw1090 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw1090step0 line 45
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1090 line 47
  11. def OAI.MUB6.Certificate.PairSemantics.raw1091 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw1091step0 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1091 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw1092 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw1092step0 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw1092step1 line 73
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1092 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw1093 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw1093step0 line 90
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1093 line 92
  21. def OAI.MUB6.Certificate.PairSemantics.raw1094 line 101
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1094 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw1095 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw1095step0 line 109
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1095 line 111
  26. def OAI.MUB6.Certificate.PairSemantics.raw1096 line 120
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1096 line 122
  28. def OAI.MUB6.Certificate.PairSemantics.raw1097 line 126
  29. def OAI.MUB6.Certificate.PairSemantics.raw1097step0 line 128
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1097 line 130
  31. def OAI.MUB6.Certificate.PairSemantics.raw1098 line 139
  32. def OAI.MUB6.Certificate.PairSemantics.raw1098step0 line 141
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1098 line 143
  34. def OAI.MUB6.Certificate.PairSemantics.raw1099 line 152
  35. def OAI.MUB6.Certificate.PairSemantics.raw1099step0 line 154
  36. def OAI.MUB6.Certificate.PairSemantics.raw1099step1 line 156
  37. def OAI.MUB6.Certificate.PairSemantics.raw1099step2 line 158
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1099 line 160
  39. def OAI.MUB6.Certificate.PairSemantics.raw1100 line 177
  40. def OAI.MUB6.Certificate.PairSemantics.raw1100step0 line 179
  41. def OAI.MUB6.Certificate.PairSemantics.raw1100step1 line 181
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1100 line 183
  43. def OAI.MUB6.Certificate.PairSemantics.raw1101 line 196
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1101 line 198
  45. def OAI.MUB6.Certificate.PairSemantics.raw1102 line 202
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1102 line 204
  47. def OAI.MUB6.Certificate.PairSemantics.raw1103 line 208
  48. def OAI.MUB6.Certificate.PairSemantics.raw1103step0 line 210
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1103 line 212
  50. def OAI.MUB6.Certificate.PairSemantics.raw1104 line 221
  51. def OAI.MUB6.Certificate.PairSemantics.raw1104step0 line 223
  52. def OAI.MUB6.Certificate.PairSemantics.raw1104step1 line 225
  53. def OAI.MUB6.Certificate.PairSemantics.raw1104step2 line 227
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical1104 line 229
  55. def OAI.MUB6.Certificate.PairSemantics.raw1105 line 246
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1105 line 248
  57. def OAI.MUB6.Certificate.PairSemantics.raw1106 line 252
  58. def OAI.MUB6.Certificate.PairSemantics.raw1106step0 line 254
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1106 line 256
  60. def OAI.MUB6.Certificate.PairSemantics.raw1107 line 265
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1107 line 267
  62. def OAI.MUB6.Certificate.PairSemantics.raw1108 line 271
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1108 line 273
  64. def OAI.MUB6.Certificate.PairSemantics.raw1109 line 277
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1109 line 279
  66. def OAI.MUB6.Certificate.PairSemantics.raw1110 line 283
  67. def OAI.MUB6.Certificate.PairSemantics.raw1110step0 line 285
  68. def OAI.MUB6.Certificate.PairSemantics.raw1110step1 line 287
  69. def OAI.MUB6.Certificate.PairSemantics.raw1110step2 line 289
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1110 line 291
  71. def OAI.MUB6.Certificate.PairSemantics.raw1111 line 308
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1111 line 310
  73. def OAI.MUB6.Certificate.PairSemantics.raw1112 line 314
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1112 line 316
  75. def OAI.MUB6.Certificate.PairSemantics.raw1113 line 320
  76. def OAI.MUB6.Certificate.PairSemantics.raw1113step0 line 322
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1113 line 324
  78. def OAI.MUB6.Certificate.PairSemantics.raw1114 line 333
  79. def OAI.MUB6.Certificate.PairSemantics.raw1114step0 line 335
  80. def OAI.MUB6.Certificate.PairSemantics.raw1114step1 line 337
  81. def OAI.MUB6.Certificate.PairSemantics.raw1114step2 line 339
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1114 line 341
  83. def OAI.MUB6.Certificate.PairSemantics.raw1115 line 358
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical1115 line 360
  85. def OAI.MUB6.Certificate.PairSemantics.raw1116 line 364
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1116 line 366
  87. def OAI.MUB6.Certificate.PairSemantics.raw1117 line 370
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical1117 line 372
  89. def OAI.MUB6.Certificate.PairSemantics.raw1118 line 376
  90. def OAI.MUB6.Certificate.PairSemantics.raw1118step0 line 378
  91. def OAI.MUB6.Certificate.PairSemantics.raw1118step1 line 380
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1118 line 382
  93. def OAI.MUB6.Certificate.PairSemantics.raw1119 line 395
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical1119 line 397