OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical7.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw224 line 11
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical224 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw225 line 17
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical225 line 19
  5. def OAI.MUB6.Certificate.PairSemantics.raw226 line 23
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical226 line 25
  7. def OAI.MUB6.Certificate.PairSemantics.raw227 line 29
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical227 line 31
  9. def OAI.MUB6.Certificate.PairSemantics.raw228 line 35
  10. def OAI.MUB6.Certificate.PairSemantics.raw228step0 line 37
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical228 line 39
  12. def OAI.MUB6.Certificate.PairSemantics.raw229 line 48
  13. def OAI.MUB6.Certificate.PairSemantics.raw229step0 line 50
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical229 line 52
  15. def OAI.MUB6.Certificate.PairSemantics.raw230 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw230step0 line 63
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical230 line 65
  18. def OAI.MUB6.Certificate.PairSemantics.raw231 line 74
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical231 line 76
  20. def OAI.MUB6.Certificate.PairSemantics.raw232 line 80
  21. def OAI.MUB6.Certificate.PairSemantics.raw232step0 line 82
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical232 line 84
  23. def OAI.MUB6.Certificate.PairSemantics.raw233 line 93
  24. def OAI.MUB6.Certificate.PairSemantics.raw233step0 line 95
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical233 line 97
  26. def OAI.MUB6.Certificate.PairSemantics.raw234 line 106
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical234 line 108
  28. def OAI.MUB6.Certificate.PairSemantics.raw235 line 112
  29. def OAI.MUB6.Certificate.PairSemantics.raw235step0 line 114
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical235 line 116
  31. def OAI.MUB6.Certificate.PairSemantics.raw236 line 125
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical236 line 127
  33. def OAI.MUB6.Certificate.PairSemantics.raw237 line 131
  34. def OAI.MUB6.Certificate.PairSemantics.raw237step0 line 133
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical237 line 135
  36. def OAI.MUB6.Certificate.PairSemantics.raw238 line 144
  37. def OAI.MUB6.Certificate.PairSemantics.raw238step0 line 146
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical238 line 148
  39. def OAI.MUB6.Certificate.PairSemantics.raw239 line 157
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical239 line 159
  41. def OAI.MUB6.Certificate.PairSemantics.raw240 line 163
  42. def OAI.MUB6.Certificate.PairSemantics.raw240step0 line 165
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical240 line 167
  44. def OAI.MUB6.Certificate.PairSemantics.raw241 line 176
  45. def OAI.MUB6.Certificate.PairSemantics.raw241step0 line 178
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical241 line 180
  47. def OAI.MUB6.Certificate.PairSemantics.raw242 line 189
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical242 line 191
  49. def OAI.MUB6.Certificate.PairSemantics.raw243 line 195
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical243 line 197
  51. def OAI.MUB6.Certificate.PairSemantics.raw244 line 201
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical244 line 203
  53. def OAI.MUB6.Certificate.PairSemantics.raw245 line 207
  54. def OAI.MUB6.Certificate.PairSemantics.raw245step0 line 209
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical245 line 211
  56. def OAI.MUB6.Certificate.PairSemantics.raw246 line 220
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical246 line 222
  58. def OAI.MUB6.Certificate.PairSemantics.raw247 line 226
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical247 line 228
  60. def OAI.MUB6.Certificate.PairSemantics.raw248 line 232
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical248 line 234
  62. def OAI.MUB6.Certificate.PairSemantics.raw249 line 238
  63. def OAI.MUB6.Certificate.PairSemantics.raw249step0 line 240
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical249 line 242
  65. def OAI.MUB6.Certificate.PairSemantics.raw250 line 251
  66. def OAI.MUB6.Certificate.PairSemantics.raw250step0 line 253
  67. def OAI.MUB6.Certificate.PairSemantics.raw250step1 line 255
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical250 line 257
  69. def OAI.MUB6.Certificate.PairSemantics.raw251 line 270
  70. def OAI.MUB6.Certificate.PairSemantics.raw251step0 line 272
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical251 line 274
  72. def OAI.MUB6.Certificate.PairSemantics.raw252 line 283
  73. def OAI.MUB6.Certificate.PairSemantics.raw252step0 line 285
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical252 line 287
  75. def OAI.MUB6.Certificate.PairSemantics.raw253 line 296
  76. def OAI.MUB6.Certificate.PairSemantics.raw253step0 line 298
  77. def OAI.MUB6.Certificate.PairSemantics.raw253step1 line 300
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical253 line 302
  79. def OAI.MUB6.Certificate.PairSemantics.raw254 line 315
  80. def OAI.MUB6.Certificate.PairSemantics.raw254step0 line 317
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical254 line 319
  82. def OAI.MUB6.Certificate.PairSemantics.raw255 line 328
  83. def OAI.MUB6.Certificate.PairSemantics.raw255step0 line 330
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical255 line 332