OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical174.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5568 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5568 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw5569 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw5569step0 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw5569step1 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5569 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw5570 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw5570step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5570 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw5571 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw5571step0 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw5571step1 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5571 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw5572 line 73
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5572 line 75
  16. def OAI.MUB6.Certificate.PairSemantics.raw5573 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw5573step0 line 81
  18. def OAI.MUB6.Certificate.PairSemantics.raw5573step1 line 83
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical5573 line 85
  20. def OAI.MUB6.Certificate.PairSemantics.raw5574 line 98
  21. def OAI.MUB6.Certificate.PairSemantics.raw5574step0 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw5574step1 line 102
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5574 line 104
  24. def OAI.MUB6.Certificate.PairSemantics.raw5575 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw5575step0 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw5575step1 line 121
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical5575 line 123
  28. def OAI.MUB6.Certificate.PairSemantics.raw5576 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw5576step0 line 138
  30. def OAI.MUB6.Certificate.PairSemantics.raw5576step1 line 140
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5576 line 142
  32. def OAI.MUB6.Certificate.PairSemantics.raw5577 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw5577step0 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw5577step1 line 159
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5577 line 161
  36. def OAI.MUB6.Certificate.PairSemantics.raw5578 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw5578step0 line 176
  38. def OAI.MUB6.Certificate.PairSemantics.raw5578step1 line 178
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5578 line 180
  40. def OAI.MUB6.Certificate.PairSemantics.raw5579 line 193
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5579 line 195
  42. def OAI.MUB6.Certificate.PairSemantics.raw5580 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw5580step0 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw5580step1 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw5580step2 line 205
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5580 line 207
  47. def OAI.MUB6.Certificate.PairSemantics.raw5581 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw5581step0 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw5581step1 line 229
  50. def OAI.MUB6.Certificate.PairSemantics.raw5581step2 line 231
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5581 line 233
  52. def OAI.MUB6.Certificate.PairSemantics.raw5582 line 251
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5582 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw5583 line 257
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5583 line 259
  56. def OAI.MUB6.Certificate.PairSemantics.raw5584 line 263
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical5584 line 265
  58. def OAI.MUB6.Certificate.PairSemantics.raw5585 line 269
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5585 line 271
  60. def OAI.MUB6.Certificate.PairSemantics.raw5586 line 275
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5586 line 277
  62. def OAI.MUB6.Certificate.PairSemantics.raw5587 line 281
  63. def OAI.MUB6.Certificate.PairSemantics.raw5587step0 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw5587step1 line 285
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5587 line 287
  66. def OAI.MUB6.Certificate.PairSemantics.raw5588 line 300
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5588 line 302
  68. def OAI.MUB6.Certificate.PairSemantics.raw5589 line 306
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5589 line 308
  70. def OAI.MUB6.Certificate.PairSemantics.raw5590 line 312
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5590 line 314
  72. def OAI.MUB6.Certificate.PairSemantics.raw5591 line 318
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5591 line 320
  74. def OAI.MUB6.Certificate.PairSemantics.raw5592 line 324
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5592 line 326
  76. def OAI.MUB6.Certificate.PairSemantics.raw5593 line 330
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5593 line 332
  78. def OAI.MUB6.Certificate.PairSemantics.raw5594 line 336
  79. def OAI.MUB6.Certificate.PairSemantics.raw5594step0 line 338
  80. def OAI.MUB6.Certificate.PairSemantics.raw5594step1 line 340
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5594 line 342
  82. def OAI.MUB6.Certificate.PairSemantics.raw5595 line 355
  83. def OAI.MUB6.Certificate.PairSemantics.raw5595step0 line 357
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5595 line 359
  85. def OAI.MUB6.Certificate.PairSemantics.raw5596 line 368
  86. def OAI.MUB6.Certificate.PairSemantics.raw5596step0 line 370
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5596 line 372
  88. def OAI.MUB6.Certificate.PairSemantics.raw5597 line 381
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5597 line 383
  90. def OAI.MUB6.Certificate.PairSemantics.raw5598 line 387
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5598 line 389
  92. def OAI.MUB6.Certificate.PairSemantics.raw5599 line 393
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5599 line 395