OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical125.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4000 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4000 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw4001 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4001 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw4002 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw4002step0 line 27
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4002 line 29
  8. def OAI.MUB6.Certificate.PairSemantics.raw4003 line 38
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4003 line 40
  10. def OAI.MUB6.Certificate.PairSemantics.raw4004 line 44
  11. def OAI.MUB6.Certificate.PairSemantics.raw4004step0 line 46
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4004 line 48
  13. def OAI.MUB6.Certificate.PairSemantics.raw4005 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw4005step0 line 59
  15. def OAI.MUB6.Certificate.PairSemantics.raw4005step1 line 61
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4005 line 63
  17. def OAI.MUB6.Certificate.PairSemantics.raw4006 line 76
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4006 line 78
  19. def OAI.MUB6.Certificate.PairSemantics.raw4007 line 82
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4007 line 84
  21. def OAI.MUB6.Certificate.PairSemantics.raw4008 line 88
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4008 line 90
  23. def OAI.MUB6.Certificate.PairSemantics.raw4009 line 94
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4009 line 96
  25. def OAI.MUB6.Certificate.PairSemantics.raw4010 line 100
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4010 line 102
  27. def OAI.MUB6.Certificate.PairSemantics.raw4011 line 106
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4011 line 108
  29. def OAI.MUB6.Certificate.PairSemantics.raw4012 line 112
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4012 line 114
  31. def OAI.MUB6.Certificate.PairSemantics.raw4013 line 118
  32. def OAI.MUB6.Certificate.PairSemantics.raw4013step0 line 120
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4013 line 122
  34. def OAI.MUB6.Certificate.PairSemantics.raw4014 line 131
  35. def OAI.MUB6.Certificate.PairSemantics.raw4014step0 line 133
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4014 line 135
  37. def OAI.MUB6.Certificate.PairSemantics.raw4015 line 144
  38. def OAI.MUB6.Certificate.PairSemantics.raw4015step0 line 146
  39. def OAI.MUB6.Certificate.PairSemantics.raw4015step1 line 148
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4015 line 150
  41. def OAI.MUB6.Certificate.PairSemantics.raw4016 line 163
  42. def OAI.MUB6.Certificate.PairSemantics.raw4016step0 line 165
  43. def OAI.MUB6.Certificate.PairSemantics.raw4016step1 line 167
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4016 line 169
  45. def OAI.MUB6.Certificate.PairSemantics.raw4017 line 182
  46. def OAI.MUB6.Certificate.PairSemantics.raw4017step0 line 184
  47. def OAI.MUB6.Certificate.PairSemantics.raw4017step1 line 186
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4017 line 188
  49. def OAI.MUB6.Certificate.PairSemantics.raw4018 line 201
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4018 line 203
  51. def OAI.MUB6.Certificate.PairSemantics.raw4019 line 207
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4019 line 209
  53. def OAI.MUB6.Certificate.PairSemantics.raw4020 line 213
  54. def OAI.MUB6.Certificate.PairSemantics.raw4020step0 line 215
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4020 line 217
  56. def OAI.MUB6.Certificate.PairSemantics.raw4021 line 227
  57. def OAI.MUB6.Certificate.PairSemantics.raw4021step0 line 229
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4021 line 231
  59. def OAI.MUB6.Certificate.PairSemantics.raw4022 line 241
  60. def OAI.MUB6.Certificate.PairSemantics.raw4022step0 line 243
  61. def OAI.MUB6.Certificate.PairSemantics.raw4022step1 line 245
  62. def OAI.MUB6.Certificate.PairSemantics.raw4022step2 line 247
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical4022 line 249
  64. def OAI.MUB6.Certificate.PairSemantics.raw4023 line 267
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4023 line 269
  66. def OAI.MUB6.Certificate.PairSemantics.raw4024 line 273
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4024 line 275
  68. def OAI.MUB6.Certificate.PairSemantics.raw4025 line 279
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4025 line 281
  70. def OAI.MUB6.Certificate.PairSemantics.raw4026 line 285
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4026 line 287
  72. def OAI.MUB6.Certificate.PairSemantics.raw4027 line 291
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4027 line 293
  74. def OAI.MUB6.Certificate.PairSemantics.raw4028 line 297
  75. def OAI.MUB6.Certificate.PairSemantics.raw4028step0 line 299
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4028 line 301
  77. def OAI.MUB6.Certificate.PairSemantics.raw4029 line 310
  78. def OAI.MUB6.Certificate.PairSemantics.raw4029step0 line 312
  79. def OAI.MUB6.Certificate.PairSemantics.raw4029step1 line 314
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4029 line 316
  81. def OAI.MUB6.Certificate.PairSemantics.raw4030 line 329
  82. def OAI.MUB6.Certificate.PairSemantics.raw4030step0 line 331
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4030 line 333
  84. def OAI.MUB6.Certificate.PairSemantics.raw4031 line 343
  85. def OAI.MUB6.Certificate.PairSemantics.raw4031step0 line 345
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4031 line 347