OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical9.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw288 line 14
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical288 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw289 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical289 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw290 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical290 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw291 line 32
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical291 line 34
  9. def OAI.MUB6.Certificate.PairSemantics.raw292 line 38
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical292 line 40
  11. def OAI.MUB6.Certificate.PairSemantics.raw293 line 44
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical293 line 46
  13. def OAI.MUB6.Certificate.PairSemantics.raw294 line 50
  14. def OAI.MUB6.Certificate.PairSemantics.raw294step0 line 52
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical294 line 54
  16. def OAI.MUB6.Certificate.PairSemantics.raw295 line 63
  17. def OAI.MUB6.Certificate.PairSemantics.raw295step0 line 65
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical295 line 67
  19. def OAI.MUB6.Certificate.PairSemantics.raw296 line 76
  20. def OAI.MUB6.Certificate.PairSemantics.raw296step0 line 78
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical296 line 80
  22. def OAI.MUB6.Certificate.PairSemantics.raw297 line 89
  23. def OAI.MUB6.Certificate.PairSemantics.raw297step0 line 91
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical297 line 93
  25. def OAI.MUB6.Certificate.PairSemantics.raw298 line 102
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical298 line 104
  27. def OAI.MUB6.Certificate.PairSemantics.raw299 line 108
  28. def OAI.MUB6.Certificate.PairSemantics.raw299step0 line 110
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical299 line 112
  30. def OAI.MUB6.Certificate.PairSemantics.raw300 line 121
  31. def OAI.MUB6.Certificate.PairSemantics.raw300step0 line 123
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical300 line 125
  33. def OAI.MUB6.Certificate.PairSemantics.raw301 line 134
  34. def OAI.MUB6.Certificate.PairSemantics.raw301step0 line 136
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical301 line 138
  36. def OAI.MUB6.Certificate.PairSemantics.raw302 line 147
  37. def OAI.MUB6.Certificate.PairSemantics.raw302step0 line 149
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical302 line 151
  39. def OAI.MUB6.Certificate.PairSemantics.raw303 line 160
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical303 line 162
  41. def OAI.MUB6.Certificate.PairSemantics.raw304 line 166
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical304 line 168
  43. def OAI.MUB6.Certificate.PairSemantics.raw305 line 172
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical305 line 174
  45. def OAI.MUB6.Certificate.PairSemantics.raw306 line 178
  46. def OAI.MUB6.Certificate.PairSemantics.raw306step0 line 180
  47. def OAI.MUB6.Certificate.PairSemantics.raw306step1 line 182
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical306 line 184
  49. def OAI.MUB6.Certificate.PairSemantics.raw307 line 197
  50. def OAI.MUB6.Certificate.PairSemantics.raw307step0 line 199
  51. def OAI.MUB6.Certificate.PairSemantics.raw307step1 line 201
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical307 line 203
  53. def OAI.MUB6.Certificate.PairSemantics.raw308 line 216
  54. def OAI.MUB6.Certificate.PairSemantics.raw308step0 line 218
  55. def OAI.MUB6.Certificate.PairSemantics.raw308step1 line 220
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical308 line 222
  57. def OAI.MUB6.Certificate.PairSemantics.raw309 line 235
  58. def OAI.MUB6.Certificate.PairSemantics.raw309step0 line 237
  59. def OAI.MUB6.Certificate.PairSemantics.raw309step1 line 239
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical309 line 241
  61. def OAI.MUB6.Certificate.PairSemantics.raw310 line 254
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical310 line 256
  63. def OAI.MUB6.Certificate.PairSemantics.raw311 line 260
  64. def OAI.MUB6.Certificate.PairSemantics.raw311step0 line 262
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical311 line 264
  66. def OAI.MUB6.Certificate.PairSemantics.raw312 line 273
  67. def OAI.MUB6.Certificate.PairSemantics.raw312step0 line 275
  68. def OAI.MUB6.Certificate.PairSemantics.raw312step1 line 277
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical312 line 279
  70. def OAI.MUB6.Certificate.PairSemantics.raw313 line 292
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical313 line 294
  72. def OAI.MUB6.Certificate.PairSemantics.raw314 line 298
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical314 line 300
  74. def OAI.MUB6.Certificate.PairSemantics.raw315 line 304
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical315 line 306
  76. def OAI.MUB6.Certificate.PairSemantics.raw316 line 310
  77. def OAI.MUB6.Certificate.PairSemantics.raw316step0 line 312
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical316 line 314
  79. def OAI.MUB6.Certificate.PairSemantics.raw317 line 323
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical317 line 325
  81. def OAI.MUB6.Certificate.PairSemantics.raw318 line 329
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical318 line 331
  83. def OAI.MUB6.Certificate.PairSemantics.raw319 line 335
  84. def OAI.MUB6.Certificate.PairSemantics.raw319step0 line 337
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical319 line 339