OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical17.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw544 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw544step0 line 15
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical544 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw545 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical545 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw546 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw546step0 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical546 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw547 line 45
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical547 line 47
  11. def OAI.MUB6.Certificate.PairSemantics.raw548 line 51
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical548 line 53
  13. def OAI.MUB6.Certificate.PairSemantics.raw549 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw549step0 line 59
  15. def OAI.MUB6.Certificate.PairSemantics.raw549step1 line 61
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical549 line 63
  17. def OAI.MUB6.Certificate.PairSemantics.raw550 line 76
  18. def OAI.MUB6.Certificate.PairSemantics.raw550step0 line 78
  19. def OAI.MUB6.Certificate.PairSemantics.raw550step1 line 80
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical550 line 82
  21. def OAI.MUB6.Certificate.PairSemantics.raw551 line 95
  22. def OAI.MUB6.Certificate.PairSemantics.raw551step0 line 97
  23. def OAI.MUB6.Certificate.PairSemantics.raw551step1 line 99
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical551 line 101
  25. def OAI.MUB6.Certificate.PairSemantics.raw552 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw552step0 line 116
  27. def OAI.MUB6.Certificate.PairSemantics.raw552step1 line 118
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical552 line 120
  29. def OAI.MUB6.Certificate.PairSemantics.raw553 line 133
  30. def OAI.MUB6.Certificate.PairSemantics.raw553step0 line 135
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical553 line 137
  32. def OAI.MUB6.Certificate.PairSemantics.raw554 line 146
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical554 line 148
  34. def OAI.MUB6.Certificate.PairSemantics.raw555 line 152
  35. def OAI.MUB6.Certificate.PairSemantics.raw555step0 line 154
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical555 line 156
  37. def OAI.MUB6.Certificate.PairSemantics.raw556 line 165
  38. def OAI.MUB6.Certificate.PairSemantics.raw556step0 line 167
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical556 line 169
  40. def OAI.MUB6.Certificate.PairSemantics.raw557 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw557step0 line 180
  42. def OAI.MUB6.Certificate.PairSemantics.raw557step1 line 182
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical557 line 184
  44. def OAI.MUB6.Certificate.PairSemantics.raw558 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw558step0 line 199
  46. def OAI.MUB6.Certificate.PairSemantics.raw558step1 line 201
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical558 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw559 line 216
  49. def OAI.MUB6.Certificate.PairSemantics.raw559step0 line 218
  50. def OAI.MUB6.Certificate.PairSemantics.raw559step1 line 220
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical559 line 222
  52. def OAI.MUB6.Certificate.PairSemantics.raw560 line 235
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical560 line 237
  54. def OAI.MUB6.Certificate.PairSemantics.raw561 line 241
  55. def OAI.MUB6.Certificate.PairSemantics.raw561step0 line 243
  56. def OAI.MUB6.Certificate.PairSemantics.raw561step1 line 245
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical561 line 247
  58. def OAI.MUB6.Certificate.PairSemantics.raw562 line 260
  59. def OAI.MUB6.Certificate.PairSemantics.raw562step0 line 262
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical562 line 264
  61. def OAI.MUB6.Certificate.PairSemantics.raw563 line 273
  62. def OAI.MUB6.Certificate.PairSemantics.raw563step0 line 275
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical563 line 277
  64. def OAI.MUB6.Certificate.PairSemantics.raw564 line 286
  65. def OAI.MUB6.Certificate.PairSemantics.raw564step0 line 288
  66. def OAI.MUB6.Certificate.PairSemantics.raw564step1 line 290
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical564 line 292
  68. def OAI.MUB6.Certificate.PairSemantics.raw565 line 305
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical565 line 307
  70. def OAI.MUB6.Certificate.PairSemantics.raw566 line 311
  71. def OAI.MUB6.Certificate.PairSemantics.raw566step0 line 313
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical566 line 315
  73. def OAI.MUB6.Certificate.PairSemantics.raw567 line 324
  74. def OAI.MUB6.Certificate.PairSemantics.raw567step0 line 326
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical567 line 328
  76. def OAI.MUB6.Certificate.PairSemantics.raw568 line 337
  77. def OAI.MUB6.Certificate.PairSemantics.raw568step0 line 339
  78. def OAI.MUB6.Certificate.PairSemantics.raw568step1 line 341
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical568 line 343
  80. def OAI.MUB6.Certificate.PairSemantics.raw569 line 356
  81. def OAI.MUB6.Certificate.PairSemantics.raw569step0 line 358
  82. def OAI.MUB6.Certificate.PairSemantics.raw569step1 line 360
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical569 line 362
  84. def OAI.MUB6.Certificate.PairSemantics.raw570 line 375
  85. def OAI.MUB6.Certificate.PairSemantics.raw570step0 line 377
  86. def OAI.MUB6.Certificate.PairSemantics.raw570step1 line 379
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical570 line 381
  88. def OAI.MUB6.Certificate.PairSemantics.raw571 line 394
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical571 line 396
  90. def OAI.MUB6.Certificate.PairSemantics.raw572 line 400
  91. def OAI.MUB6.Certificate.PairSemantics.raw572step0 line 402
  92. def OAI.MUB6.Certificate.PairSemantics.raw572step1 line 404
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical572 line 406
  94. def OAI.MUB6.Certificate.PairSemantics.raw573 line 419
  95. def OAI.MUB6.Certificate.PairSemantics.raw573step0 line 421
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical573 line 423
  97. def OAI.MUB6.Certificate.PairSemantics.raw574 line 432
  98. def OAI.MUB6.Certificate.PairSemantics.raw574step0 line 434
  99. def OAI.MUB6.Certificate.PairSemantics.raw574step1 line 436
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical574 line 438
  101. def OAI.MUB6.Certificate.PairSemantics.raw575 line 451
  102. def OAI.MUB6.Certificate.PairSemantics.raw575step0 line 453
  103. def OAI.MUB6.Certificate.PairSemantics.raw575step1 line 455
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical575 line 457