OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical225.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7200 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw7200step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw7200step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7200 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw7201 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw7201step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw7201step1 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw7201step2 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7201 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw7202 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw7202step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw7202step1 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw7202step2 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical7202 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw7203 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw7203step0 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw7203step1 line 92
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical7203 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw7204 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw7204step0 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw7204step1 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7204 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7205 line 126
  24. def OAI.MUB6.Certificate.PairSemantics.raw7205step0 line 128
  25. def OAI.MUB6.Certificate.PairSemantics.raw7205step1 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw7205step2 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw7205step3 line 134
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7205 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw7206 line 158
  30. def OAI.MUB6.Certificate.PairSemantics.raw7206step0 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw7206step1 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw7206step2 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw7206step3 line 166
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7206 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw7207 line 191
  36. def OAI.MUB6.Certificate.PairSemantics.raw7207step0 line 193
  37. def OAI.MUB6.Certificate.PairSemantics.raw7207step1 line 195
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7207 line 197
  39. def OAI.MUB6.Certificate.PairSemantics.raw7208 line 212
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7208 line 214
  41. def OAI.MUB6.Certificate.PairSemantics.raw7209 line 218
  42. def OAI.MUB6.Certificate.PairSemantics.raw7209step0 line 220
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7209 line 222
  44. def OAI.MUB6.Certificate.PairSemantics.raw7210 line 232
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7210 line 234
  46. def OAI.MUB6.Certificate.PairSemantics.raw7211 line 238
  47. def OAI.MUB6.Certificate.PairSemantics.raw7211step0 line 240
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7211 line 242
  49. def OAI.MUB6.Certificate.PairSemantics.raw7212 line 251
  50. def OAI.MUB6.Certificate.PairSemantics.raw7212step0 line 253
  51. def OAI.MUB6.Certificate.PairSemantics.raw7212step1 line 255
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7212 line 257
  53. def OAI.MUB6.Certificate.PairSemantics.raw7213 line 270
  54. def OAI.MUB6.Certificate.PairSemantics.raw7213step0 line 272
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7213 line 274
  56. def OAI.MUB6.Certificate.PairSemantics.raw7214 line 284
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7214 line 286
  58. def OAI.MUB6.Certificate.PairSemantics.raw7215 line 290
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7215 line 292
  60. def OAI.MUB6.Certificate.PairSemantics.raw7216 line 296
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7216 line 298
  62. def OAI.MUB6.Certificate.PairSemantics.raw7217 line 302
  63. def OAI.MUB6.Certificate.PairSemantics.raw7217step0 line 304
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical7217 line 306
  65. def OAI.MUB6.Certificate.PairSemantics.raw7218 line 315
  66. def OAI.MUB6.Certificate.PairSemantics.raw7218step0 line 317
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical7218 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw7219 line 329
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7219 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw7220 line 335
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7220 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw7221 line 341
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical7221 line 343
  74. def OAI.MUB6.Certificate.PairSemantics.raw7222 line 347
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7222 line 349
  76. def OAI.MUB6.Certificate.PairSemantics.raw7223 line 353
  77. def OAI.MUB6.Certificate.PairSemantics.raw7223step0 line 355
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7223 line 357
  79. def OAI.MUB6.Certificate.PairSemantics.raw7224 line 367
  80. def OAI.MUB6.Certificate.PairSemantics.raw7224step0 line 369
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical7224 line 371
  82. def OAI.MUB6.Certificate.PairSemantics.raw7225 line 380
  83. def OAI.MUB6.Certificate.PairSemantics.raw7225step0 line 382
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7225 line 384
  85. def OAI.MUB6.Certificate.PairSemantics.raw7226 line 393
  86. def OAI.MUB6.Certificate.PairSemantics.raw7226step0 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw7226step1 line 397
  88. def OAI.MUB6.Certificate.PairSemantics.raw7226step2 line 399
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7226 line 401
  90. def OAI.MUB6.Certificate.PairSemantics.raw7227 line 418
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7227 line 420
  92. def OAI.MUB6.Certificate.PairSemantics.raw7228 line 424
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7228 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw7229 line 430
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7229 line 432
  96. def OAI.MUB6.Certificate.PairSemantics.raw7230 line 436
  97. def OAI.MUB6.Certificate.PairSemantics.raw7230step0 line 438
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7230 line 440
  99. def OAI.MUB6.Certificate.PairSemantics.raw7231 line 449
  100. def OAI.MUB6.Certificate.PairSemantics.raw7231step0 line 451
  101. def OAI.MUB6.Certificate.PairSemantics.raw7231step1 line 453
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical7231 line 455