OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical198.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6336 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw6336step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw6336step1 line 26
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6336 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw6337 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw6337step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw6337step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6337 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw6338 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw6338step0 line 62
  11. def OAI.MUB6.Certificate.PairSemantics.raw6338step1 line 64
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6338 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw6339 line 79
  14. def OAI.MUB6.Certificate.PairSemantics.raw6339step0 line 81
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6339 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw6340 line 92
  17. def OAI.MUB6.Certificate.PairSemantics.raw6340step0 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw6340step1 line 96
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6340 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw6341 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw6341step0 line 113
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6341 line 115
  23. def OAI.MUB6.Certificate.PairSemantics.raw6342 line 124
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6342 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw6343 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw6343step0 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6343 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw6344 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw6344step0 line 145
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6344 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw6345 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw6345step0 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw6345step1 line 160
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6345 line 162
  35. def OAI.MUB6.Certificate.PairSemantics.raw6346 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw6346step0 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw6346step1 line 179
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6346 line 181
  39. def OAI.MUB6.Certificate.PairSemantics.raw6347 line 194
  40. def OAI.MUB6.Certificate.PairSemantics.raw6347step0 line 196
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6347 line 198
  42. def OAI.MUB6.Certificate.PairSemantics.raw6348 line 207
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6348 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw6349 line 213
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6349 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw6350 line 219
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6350 line 221
  48. def OAI.MUB6.Certificate.PairSemantics.raw6351 line 225
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6351 line 227
  50. def OAI.MUB6.Certificate.PairSemantics.raw6352 line 231
  51. def OAI.MUB6.Certificate.PairSemantics.raw6352step0 line 233
  52. def OAI.MUB6.Certificate.PairSemantics.raw6352step1 line 235
  53. def OAI.MUB6.Certificate.PairSemantics.raw6352step2 line 237
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6352 line 239
  55. def OAI.MUB6.Certificate.PairSemantics.raw6353 line 256
  56. def OAI.MUB6.Certificate.PairSemantics.raw6353step0 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw6353step1 line 260
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6353 line 262
  59. def OAI.MUB6.Certificate.PairSemantics.raw6354 line 275
  60. def OAI.MUB6.Certificate.PairSemantics.raw6354step0 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw6354step1 line 279
  62. def OAI.MUB6.Certificate.PairSemantics.raw6354step2 line 281
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6354 line 283
  64. def OAI.MUB6.Certificate.PairSemantics.raw6355 line 300
  65. def OAI.MUB6.Certificate.PairSemantics.raw6355step0 line 302
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6355 line 304
  67. def OAI.MUB6.Certificate.PairSemantics.raw6356 line 313
  68. def OAI.MUB6.Certificate.PairSemantics.raw6356step0 line 315
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6356 line 317
  70. def OAI.MUB6.Certificate.PairSemantics.raw6357 line 326
  71. def OAI.MUB6.Certificate.PairSemantics.raw6357step0 line 328
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6357 line 330
  73. def OAI.MUB6.Certificate.PairSemantics.raw6358 line 339
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6358 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw6359 line 345
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6359 line 347
  77. def OAI.MUB6.Certificate.PairSemantics.raw6360 line 351
  78. def OAI.MUB6.Certificate.PairSemantics.raw6360step0 line 353
  79. def OAI.MUB6.Certificate.PairSemantics.raw6360step1 line 355
  80. def OAI.MUB6.Certificate.PairSemantics.raw6360step2 line 357
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6360 line 359
  82. def OAI.MUB6.Certificate.PairSemantics.raw6361 line 376
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6361 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw6362 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw6362step0 line 384
  86. def OAI.MUB6.Certificate.PairSemantics.raw6362step1 line 386
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical6362 line 388
  88. def OAI.MUB6.Certificate.PairSemantics.raw6363 line 401
  89. def OAI.MUB6.Certificate.PairSemantics.raw6363step0 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw6363step1 line 405
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6363 line 407
  92. def OAI.MUB6.Certificate.PairSemantics.raw6364 line 420
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6364 line 422
  94. def OAI.MUB6.Certificate.PairSemantics.raw6365 line 426
  95. def OAI.MUB6.Certificate.PairSemantics.raw6365step0 line 428
  96. def OAI.MUB6.Certificate.PairSemantics.raw6365step1 line 430
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6365 line 432
  98. def OAI.MUB6.Certificate.PairSemantics.raw6366 line 445
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6366 line 447
  100. def OAI.MUB6.Certificate.PairSemantics.raw6367 line 451
  101. def OAI.MUB6.Certificate.PairSemantics.raw6367step0 line 453
  102. def OAI.MUB6.Certificate.PairSemantics.raw6367step1 line 455
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6367 line 457