OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical186.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5952 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw5952step0 line 12
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5952 line 14
  4. def OAI.MUB6.Certificate.PairSemantics.raw5953 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw5953step0 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5953 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw5954 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw5954step0 line 38
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5954 line 40
  10. def OAI.MUB6.Certificate.PairSemantics.raw5955 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw5955step0 line 52
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5955 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw5956 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw5956step0 line 66
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5956 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw5957 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw5957step0 line 80
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical5957 line 82
  19. def OAI.MUB6.Certificate.PairSemantics.raw5958 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw5958step0 line 93
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5958 line 95
  22. def OAI.MUB6.Certificate.PairSemantics.raw5959 line 105
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5959 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw5960 line 111
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5960 line 113
  26. def OAI.MUB6.Certificate.PairSemantics.raw5961 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw5961step0 line 119
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5961 line 121
  29. def OAI.MUB6.Certificate.PairSemantics.raw5962 line 130
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5962 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw5963 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw5963step0 line 138
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5963 line 140
  34. def OAI.MUB6.Certificate.PairSemantics.raw5964 line 149
  35. def OAI.MUB6.Certificate.PairSemantics.raw5964step0 line 151
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5964 line 153
  37. def OAI.MUB6.Certificate.PairSemantics.raw5965 line 162
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5965 line 164
  39. def OAI.MUB6.Certificate.PairSemantics.raw5966 line 168
  40. def OAI.MUB6.Certificate.PairSemantics.raw5966step0 line 170
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5966 line 172
  42. def OAI.MUB6.Certificate.PairSemantics.raw5967 line 182
  43. def OAI.MUB6.Certificate.PairSemantics.raw5967step0 line 184
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5967 line 186
  45. def OAI.MUB6.Certificate.PairSemantics.raw5968 line 195
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5968 line 197
  47. def OAI.MUB6.Certificate.PairSemantics.raw5969 line 201
  48. def OAI.MUB6.Certificate.PairSemantics.raw5969step0 line 203
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5969 line 205
  50. def OAI.MUB6.Certificate.PairSemantics.raw5970 line 214
  51. def OAI.MUB6.Certificate.PairSemantics.raw5970step0 line 216
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5970 line 218
  53. def OAI.MUB6.Certificate.PairSemantics.raw5971 line 227
  54. def OAI.MUB6.Certificate.PairSemantics.raw5971step0 line 229
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5971 line 231
  56. def OAI.MUB6.Certificate.PairSemantics.raw5972 line 240
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical5972 line 242
  58. def OAI.MUB6.Certificate.PairSemantics.raw5973 line 246
  59. def OAI.MUB6.Certificate.PairSemantics.raw5973step0 line 248
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5973 line 250
  61. def OAI.MUB6.Certificate.PairSemantics.raw5974 line 259
  62. def OAI.MUB6.Certificate.PairSemantics.raw5974step0 line 261
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5974 line 263
  64. def OAI.MUB6.Certificate.PairSemantics.raw5975 line 273
  65. def OAI.MUB6.Certificate.PairSemantics.raw5975step0 line 275
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5975 line 277
  67. def OAI.MUB6.Certificate.PairSemantics.raw5976 line 286
  68. def OAI.MUB6.Certificate.PairSemantics.raw5976step0 line 288
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5976 line 290
  70. def OAI.MUB6.Certificate.PairSemantics.raw5977 line 299
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5977 line 301
  72. def OAI.MUB6.Certificate.PairSemantics.raw5978 line 305
  73. def OAI.MUB6.Certificate.PairSemantics.raw5978step0 line 307
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5978 line 309
  75. def OAI.MUB6.Certificate.PairSemantics.raw5979 line 318
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5979 line 320
  77. def OAI.MUB6.Certificate.PairSemantics.raw5980 line 324
  78. def OAI.MUB6.Certificate.PairSemantics.raw5980step0 line 326
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5980 line 328
  80. def OAI.MUB6.Certificate.PairSemantics.raw5981 line 337
  81. def OAI.MUB6.Certificate.PairSemantics.raw5981step0 line 339
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical5981 line 341
  83. def OAI.MUB6.Certificate.PairSemantics.raw5982 line 350
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5982 line 352
  85. def OAI.MUB6.Certificate.PairSemantics.raw5983 line 356
  86. def OAI.MUB6.Certificate.PairSemantics.raw5983step0 line 358
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5983 line 360