OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical173.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5536 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5536 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw5537 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw5537step0 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5537 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw5538 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw5538step0 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5538 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw5539 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw5539step0 line 47
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5539 line 49
  12. def OAI.MUB6.Certificate.PairSemantics.raw5540 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5540 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw5541 line 64
  15. def OAI.MUB6.Certificate.PairSemantics.raw5541step0 line 66
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5541 line 68
  17. def OAI.MUB6.Certificate.PairSemantics.raw5542 line 78
  18. def OAI.MUB6.Certificate.PairSemantics.raw5542step0 line 80
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5542 line 82
  20. def OAI.MUB6.Certificate.PairSemantics.raw5543 line 91
  21. def OAI.MUB6.Certificate.PairSemantics.raw5543step0 line 93
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5543 line 95
  23. def OAI.MUB6.Certificate.PairSemantics.raw5544 line 104
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5544 line 106
  25. def OAI.MUB6.Certificate.PairSemantics.raw5545 line 110
  26. def OAI.MUB6.Certificate.PairSemantics.raw5545step0 line 112
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5545 line 114
  28. def OAI.MUB6.Certificate.PairSemantics.raw5546 line 123
  29. def OAI.MUB6.Certificate.PairSemantics.raw5546step0 line 125
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5546 line 127
  31. def OAI.MUB6.Certificate.PairSemantics.raw5547 line 136
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5547 line 138
  33. def OAI.MUB6.Certificate.PairSemantics.raw5548 line 142
  34. def OAI.MUB6.Certificate.PairSemantics.raw5548step0 line 144
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5548 line 146
  36. def OAI.MUB6.Certificate.PairSemantics.raw5549 line 156
  37. def OAI.MUB6.Certificate.PairSemantics.raw5549step0 line 158
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5549 line 160
  39. def OAI.MUB6.Certificate.PairSemantics.raw5550 line 169
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5550 line 171
  41. def OAI.MUB6.Certificate.PairSemantics.raw5551 line 175
  42. def OAI.MUB6.Certificate.PairSemantics.raw5551step0 line 177
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5551 line 179
  44. def OAI.MUB6.Certificate.PairSemantics.raw5552 line 189
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5552 line 191
  46. def OAI.MUB6.Certificate.PairSemantics.raw5553 line 195
  47. def OAI.MUB6.Certificate.PairSemantics.raw5553step0 line 197
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5553 line 199
  49. def OAI.MUB6.Certificate.PairSemantics.raw5554 line 208
  50. def OAI.MUB6.Certificate.PairSemantics.raw5554step0 line 210
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5554 line 212
  52. def OAI.MUB6.Certificate.PairSemantics.raw5555 line 221
  53. def OAI.MUB6.Certificate.PairSemantics.raw5555step0 line 223
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5555 line 225
  55. def OAI.MUB6.Certificate.PairSemantics.raw5556 line 234
  56. def OAI.MUB6.Certificate.PairSemantics.raw5556step0 line 236
  57. def OAI.MUB6.Certificate.PairSemantics.raw5556step1 line 238
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5556 line 240
  59. def OAI.MUB6.Certificate.PairSemantics.raw5557 line 253
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5557 line 255
  61. def OAI.MUB6.Certificate.PairSemantics.raw5558 line 259
  62. def OAI.MUB6.Certificate.PairSemantics.raw5558step0 line 261
  63. def OAI.MUB6.Certificate.PairSemantics.raw5558step1 line 263
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5558 line 265
  65. def OAI.MUB6.Certificate.PairSemantics.raw5559 line 278
  66. def OAI.MUB6.Certificate.PairSemantics.raw5559step0 line 280
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5559 line 282
  68. def OAI.MUB6.Certificate.PairSemantics.raw5560 line 291
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5560 line 293
  70. def OAI.MUB6.Certificate.PairSemantics.raw5561 line 297
  71. def OAI.MUB6.Certificate.PairSemantics.raw5561step0 line 299
  72. def OAI.MUB6.Certificate.PairSemantics.raw5561step1 line 301
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5561 line 303
  74. def OAI.MUB6.Certificate.PairSemantics.raw5562 line 316
  75. def OAI.MUB6.Certificate.PairSemantics.raw5562step0 line 318
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5562 line 320
  77. def OAI.MUB6.Certificate.PairSemantics.raw5563 line 329
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5563 line 331
  79. def OAI.MUB6.Certificate.PairSemantics.raw5564 line 335
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5564 line 337
  81. def OAI.MUB6.Certificate.PairSemantics.raw5565 line 341
  82. def OAI.MUB6.Certificate.PairSemantics.raw5565step0 line 343
  83. def OAI.MUB6.Certificate.PairSemantics.raw5565step1 line 345
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5565 line 347
  85. def OAI.MUB6.Certificate.PairSemantics.raw5566 line 360
  86. def OAI.MUB6.Certificate.PairSemantics.raw5566step0 line 362
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5566 line 364
  88. def OAI.MUB6.Certificate.PairSemantics.raw5567 line 373
  89. def OAI.MUB6.Certificate.PairSemantics.raw5567step0 line 375
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical5567 line 377