OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical16.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw512 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw512step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw512step1 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw512step2 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical512 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw513 line 44
  7. def OAI.MUB6.Certificate.PairSemantics.raw513step0 line 46
  8. def OAI.MUB6.Certificate.PairSemantics.raw513step1 line 48
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical513 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw514 line 64
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical514 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw515 line 70
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical515 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw516 line 76
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical516 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw517 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw517step0 line 84
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical517 line 86
  19. def OAI.MUB6.Certificate.PairSemantics.raw518 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw518step0 line 97
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical518 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw519 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw519step0 line 110
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical519 line 112
  25. def OAI.MUB6.Certificate.PairSemantics.raw520 line 121
  26. def OAI.MUB6.Certificate.PairSemantics.raw520step0 line 123
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical520 line 125
  28. def OAI.MUB6.Certificate.PairSemantics.raw521 line 134
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical521 line 136
  30. def OAI.MUB6.Certificate.PairSemantics.raw522 line 140
  31. def OAI.MUB6.Certificate.PairSemantics.raw522step0 line 142
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical522 line 144
  33. def OAI.MUB6.Certificate.PairSemantics.raw523 line 153
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical523 line 155
  35. def OAI.MUB6.Certificate.PairSemantics.raw524 line 159
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical524 line 161
  37. def OAI.MUB6.Certificate.PairSemantics.raw525 line 165
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical525 line 167
  39. def OAI.MUB6.Certificate.PairSemantics.raw526 line 171
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical526 line 173
  41. def OAI.MUB6.Certificate.PairSemantics.raw527 line 177
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical527 line 179
  43. def OAI.MUB6.Certificate.PairSemantics.raw528 line 183
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical528 line 185
  45. def OAI.MUB6.Certificate.PairSemantics.raw529 line 189
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical529 line 191
  47. def OAI.MUB6.Certificate.PairSemantics.raw530 line 195
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical530 line 197
  49. def OAI.MUB6.Certificate.PairSemantics.raw531 line 201
  50. def OAI.MUB6.Certificate.PairSemantics.raw531step0 line 203
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical531 line 205
  52. def OAI.MUB6.Certificate.PairSemantics.raw532 line 214
  53. def OAI.MUB6.Certificate.PairSemantics.raw532step0 line 216
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical532 line 218
  55. def OAI.MUB6.Certificate.PairSemantics.raw533 line 227
  56. def OAI.MUB6.Certificate.PairSemantics.raw533step0 line 229
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical533 line 231
  58. def OAI.MUB6.Certificate.PairSemantics.raw534 line 240
  59. def OAI.MUB6.Certificate.PairSemantics.raw534step0 line 242
  60. def OAI.MUB6.Certificate.PairSemantics.raw534step1 line 244
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical534 line 246
  62. def OAI.MUB6.Certificate.PairSemantics.raw535 line 259
  63. def OAI.MUB6.Certificate.PairSemantics.raw535step0 line 261
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical535 line 263
  65. def OAI.MUB6.Certificate.PairSemantics.raw536 line 272
  66. def OAI.MUB6.Certificate.PairSemantics.raw536step0 line 274
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical536 line 276
  68. def OAI.MUB6.Certificate.PairSemantics.raw537 line 285
  69. def OAI.MUB6.Certificate.PairSemantics.raw537step0 line 287
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical537 line 289
  71. def OAI.MUB6.Certificate.PairSemantics.raw538 line 298
  72. def OAI.MUB6.Certificate.PairSemantics.raw538step0 line 300
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical538 line 302
  74. def OAI.MUB6.Certificate.PairSemantics.raw539 line 311
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical539 line 313
  76. def OAI.MUB6.Certificate.PairSemantics.raw540 line 317
  77. def OAI.MUB6.Certificate.PairSemantics.raw540step0 line 319
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical540 line 321
  79. def OAI.MUB6.Certificate.PairSemantics.raw541 line 330
  80. def OAI.MUB6.Certificate.PairSemantics.raw541step0 line 332
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical541 line 334
  82. def OAI.MUB6.Certificate.PairSemantics.raw542 line 343
  83. def OAI.MUB6.Certificate.PairSemantics.raw542step0 line 345
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical542 line 347
  85. def OAI.MUB6.Certificate.PairSemantics.raw543 line 356
  86. def OAI.MUB6.Certificate.PairSemantics.raw543step0 line 358
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical543 line 360