OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical196.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6272 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw6272step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6272 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw6273 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw6273step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6273 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw6274 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw6274step0 line 42
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6274 line 44
  10. def OAI.MUB6.Certificate.PairSemantics.raw6275 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw6275step0 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6275 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw6276 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw6276step0 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6276 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw6277 line 79
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6277 line 81
  18. def OAI.MUB6.Certificate.PairSemantics.raw6278 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw6278step0 line 87
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6278 line 89
  21. def OAI.MUB6.Certificate.PairSemantics.raw6279 line 98
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6279 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw6280 line 104
  24. def OAI.MUB6.Certificate.PairSemantics.raw6280step0 line 106
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6280 line 108
  26. def OAI.MUB6.Certificate.PairSemantics.raw6281 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw6281step0 line 119
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6281 line 121
  29. def OAI.MUB6.Certificate.PairSemantics.raw6282 line 130
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6282 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw6283 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw6283step0 line 138
  33. def OAI.MUB6.Certificate.PairSemantics.raw6283step1 line 140
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6283 line 142
  35. def OAI.MUB6.Certificate.PairSemantics.raw6284 line 155
  36. def OAI.MUB6.Certificate.PairSemantics.raw6284step0 line 157
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6284 line 159
  38. def OAI.MUB6.Certificate.PairSemantics.raw6285 line 168
  39. def OAI.MUB6.Certificate.PairSemantics.raw6285step0 line 170
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6285 line 172
  41. def OAI.MUB6.Certificate.PairSemantics.raw6286 line 181
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6286 line 183
  43. def OAI.MUB6.Certificate.PairSemantics.raw6287 line 187
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6287 line 189
  45. def OAI.MUB6.Certificate.PairSemantics.raw6288 line 193
  46. def OAI.MUB6.Certificate.PairSemantics.raw6288step0 line 195
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6288 line 197
  48. def OAI.MUB6.Certificate.PairSemantics.raw6289 line 206
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6289 line 208
  50. def OAI.MUB6.Certificate.PairSemantics.raw6290 line 212
  51. def OAI.MUB6.Certificate.PairSemantics.raw6290step0 line 214
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6290 line 216
  53. def OAI.MUB6.Certificate.PairSemantics.raw6291 line 225
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6291 line 227
  55. def OAI.MUB6.Certificate.PairSemantics.raw6292 line 231
  56. def OAI.MUB6.Certificate.PairSemantics.raw6292step0 line 233
  57. def OAI.MUB6.Certificate.PairSemantics.raw6292step1 line 235
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6292 line 237
  59. def OAI.MUB6.Certificate.PairSemantics.raw6293 line 250
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6293 line 252
  61. def OAI.MUB6.Certificate.PairSemantics.raw6294 line 256
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6294 line 258
  63. def OAI.MUB6.Certificate.PairSemantics.raw6295 line 262
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6295 line 264
  65. def OAI.MUB6.Certificate.PairSemantics.raw6296 line 268
  66. def OAI.MUB6.Certificate.PairSemantics.raw6296step0 line 270
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6296 line 272
  68. def OAI.MUB6.Certificate.PairSemantics.raw6297 line 281
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6297 line 283
  70. def OAI.MUB6.Certificate.PairSemantics.raw6298 line 287
  71. def OAI.MUB6.Certificate.PairSemantics.raw6298step0 line 289
  72. def OAI.MUB6.Certificate.PairSemantics.raw6298step1 line 291
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6298 line 293
  74. def OAI.MUB6.Certificate.PairSemantics.raw6299 line 306
  75. def OAI.MUB6.Certificate.PairSemantics.raw6299step0 line 308
  76. def OAI.MUB6.Certificate.PairSemantics.raw6299step1 line 310
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6299 line 312
  78. def OAI.MUB6.Certificate.PairSemantics.raw6300 line 325
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6300 line 327
  80. def OAI.MUB6.Certificate.PairSemantics.raw6301 line 331
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6301 line 333
  82. def OAI.MUB6.Certificate.PairSemantics.raw6302 line 337
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6302 line 339
  84. def OAI.MUB6.Certificate.PairSemantics.raw6303 line 343
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6303 line 345