OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical299.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9568 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw9568step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9568 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw9569 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw9569step0 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9569 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw9570 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw9570step0 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9570 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw9571 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw9571step0 line 57
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9571 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw9572 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw9572step0 line 70
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9572 line 72
  16. def OAI.MUB6.Certificate.PairSemantics.raw9573 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw9573step0 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw9573step1 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9573 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw9574 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw9574step0 line 102
  22. def OAI.MUB6.Certificate.PairSemantics.raw9574step1 line 104
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9574 line 106
  24. def OAI.MUB6.Certificate.PairSemantics.raw9575 line 119
  25. def OAI.MUB6.Certificate.PairSemantics.raw9575step0 line 121
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9575 line 123
  27. def OAI.MUB6.Certificate.PairSemantics.raw9576 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw9576step0 line 134
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9576 line 136
  30. def OAI.MUB6.Certificate.PairSemantics.raw9577 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw9577step0 line 147
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical9577 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw9578 line 158
  34. def OAI.MUB6.Certificate.PairSemantics.raw9578step0 line 160
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical9578 line 162
  36. def OAI.MUB6.Certificate.PairSemantics.raw9579 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw9579step0 line 173
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9579 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw9580 line 184
  40. def OAI.MUB6.Certificate.PairSemantics.raw9580step0 line 186
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9580 line 188
  42. def OAI.MUB6.Certificate.PairSemantics.raw9581 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw9581step0 line 199
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9581 line 201
  45. def OAI.MUB6.Certificate.PairSemantics.raw9582 line 210
  46. def OAI.MUB6.Certificate.PairSemantics.raw9582step0 line 212
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9582 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw9583 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw9583step0 line 225
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9583 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw9584 line 236
  52. def OAI.MUB6.Certificate.PairSemantics.raw9584step0 line 238
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical9584 line 240
  54. def OAI.MUB6.Certificate.PairSemantics.raw9585 line 249
  55. def OAI.MUB6.Certificate.PairSemantics.raw9585step0 line 251
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical9585 line 253
  57. def OAI.MUB6.Certificate.PairSemantics.raw9586 line 262
  58. def OAI.MUB6.Certificate.PairSemantics.raw9586step0 line 264
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9586 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw9587 line 275
  61. def OAI.MUB6.Certificate.PairSemantics.raw9587step0 line 277
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9587 line 279
  63. def OAI.MUB6.Certificate.PairSemantics.raw9588 line 288
  64. def OAI.MUB6.Certificate.PairSemantics.raw9588step0 line 290
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9588 line 292
  66. def OAI.MUB6.Certificate.PairSemantics.raw9589 line 301
  67. def OAI.MUB6.Certificate.PairSemantics.raw9589step0 line 303
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9589 line 305
  69. def OAI.MUB6.Certificate.PairSemantics.raw9590 line 314
  70. def OAI.MUB6.Certificate.PairSemantics.raw9590step0 line 316
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9590 line 318
  72. def OAI.MUB6.Certificate.PairSemantics.raw9591 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw9591step0 line 329
  74. def OAI.MUB6.Certificate.PairSemantics.raw9591step1 line 331
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9591 line 333
  76. def OAI.MUB6.Certificate.PairSemantics.raw9592 line 346
  77. def OAI.MUB6.Certificate.PairSemantics.raw9592step0 line 348
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9592 line 350
  79. def OAI.MUB6.Certificate.PairSemantics.raw9593 line 359
  80. def OAI.MUB6.Certificate.PairSemantics.raw9593step0 line 361
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9593 line 363
  82. def OAI.MUB6.Certificate.PairSemantics.raw9594 line 372
  83. def OAI.MUB6.Certificate.PairSemantics.raw9594step0 line 374
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9594 line 376
  85. def OAI.MUB6.Certificate.PairSemantics.raw9595 line 385
  86. def OAI.MUB6.Certificate.PairSemantics.raw9595step0 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw9595step1 line 389
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9595 line 391
  89. def OAI.MUB6.Certificate.PairSemantics.raw9596 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw9596step0 line 406
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9596 line 408
  92. def OAI.MUB6.Certificate.PairSemantics.raw9597 line 417
  93. def OAI.MUB6.Certificate.PairSemantics.raw9597step0 line 419
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical9597 line 421
  95. def OAI.MUB6.Certificate.PairSemantics.raw9598 line 430
  96. def OAI.MUB6.Certificate.PairSemantics.raw9598step0 line 432
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9598 line 434
  98. def OAI.MUB6.Certificate.PairSemantics.raw9599 line 443
  99. def OAI.MUB6.Certificate.PairSemantics.raw9599step0 line 445
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9599 line 447